A Type Checker for a Logical Framework with Union and Intersection Types
International audience We present the syntax, semantics, typing, subtyping, unification, refinement, and REPL of Bull, a prototype theorem prover based on the ∆-Framework, i.e. a fully-typed Logical Framework à la Edinburgh LF decorated with union and intersection types, as described in previous pap...
Main Authors: | , |
---|---|
Other Authors: | , , , , , , , , , |
Format: | Conference Object |
Language: | English |
Published: |
HAL CCSD
2020
|
Subjects: | |
Online Access: | https://hal.archives-ouvertes.fr/hal-02573605 https://hal.archives-ouvertes.fr/hal-02573605/document https://hal.archives-ouvertes.fr/hal-02573605/file/article.pdf https://doi.org/10.4230/LIPIcs.FSCD.2020 |
id |
ftccsdartic:oai:HAL:hal-02573605v1 |
---|---|
record_format |
openpolar |
institution |
Open Polar |
collection |
Archive ouverte HAL (Hyper Article en Ligne, CCSD - Centre pour la Communication Scientifique Directe) |
op_collection_id |
ftccsdartic |
language |
English |
topic |
2012 ACM Subject Classification Theory of computation → Lambda calculus Theory of computation → Proof theory Keywords and phrases Intersection types Union types Dependent types Subtyping Type checker Refiner ∆-Framework [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL] [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] |
spellingShingle |
2012 ACM Subject Classification Theory of computation → Lambda calculus Theory of computation → Proof theory Keywords and phrases Intersection types Union types Dependent types Subtyping Type checker Refiner ∆-Framework [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL] [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Stolze, Claude Liquori, Luigi A Type Checker for a Logical Framework with Union and Intersection Types |
topic_facet |
2012 ACM Subject Classification Theory of computation → Lambda calculus Theory of computation → Proof theory Keywords and phrases Intersection types Union types Dependent types Subtyping Type checker Refiner ∆-Framework [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL] [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] |
description |
International audience We present the syntax, semantics, typing, subtyping, unification, refinement, and REPL of Bull, a prototype theorem prover based on the ∆-Framework, i.e. a fully-typed Logical Framework à la Edinburgh LF decorated with union and intersection types, as described in previous papers by the authors. Bull also implements a subtyping algorithm for the Type Theory Ξ of Barbanera-Dezani-de'Liguoro. Bull has a command-line interface where the user can declare axioms, terms, and perform computations and some basic terminal-style features like error pretty-printing, subexpressions highlighting, and file loading. Moreover, it can typecheck a proof or normalize it. These terms can be incomplete, therefore the typechecking algorithm uses unification to try to construct the missing subterms. Bull uses the syntax of Berardi's Pure Type Systems to improve the compactness and the modularity of the kernel. Abstract and concrete syntax are mostly aligned and similar to the concrete syntax of Coq. Bull uses a higher-order unification algorithm for terms, while typechecking and partial type inference are done by a bidirectional refinement algorithm, similar to the one found in Matita and Beluga. The refinement can be split into two parts: the essence refinement and the typing refinement. Binders are implemented using commonly-used de Bruijn indices. We have defined a concrete language syntax that will allow user to write ∆-terms. We have defined the reduction rules and an evaluator. We have implemented from scratch a refiner which does partial typechecking and type reconstruction. We have experimented Bull with classical examples of the intersection and union literature, such as the ones formalized by Pfenning with his Refinement Types in LF and by Pierce. We hope that this research vein could be useful to experiment, in a proof theoretical setting, forms of polymorphism alternatives to Girard's parametric one. |
author2 |
Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)) Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP) Logical Time for Formal Embedded System Design (KAIROS) COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED) Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S) Université Nice Sophia Antipolis (. - 2019) (UNS) COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (. - 2019) (UNS) COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S) COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Inria Sophia Antipolis - Méditerranée (CRISAM) Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) |
format |
Conference Object |
author |
Stolze, Claude Liquori, Luigi |
author_facet |
Stolze, Claude Liquori, Luigi |
author_sort |
Stolze, Claude |
title |
A Type Checker for a Logical Framework with Union and Intersection Types |
title_short |
A Type Checker for a Logical Framework with Union and Intersection Types |
title_full |
A Type Checker for a Logical Framework with Union and Intersection Types |
title_fullStr |
A Type Checker for a Logical Framework with Union and Intersection Types |
title_full_unstemmed |
A Type Checker for a Logical Framework with Union and Intersection Types |
title_sort |
type checker for a logical framework with union and intersection types |
publisher |
HAL CCSD |
publishDate |
2020 |
url |
https://hal.archives-ouvertes.fr/hal-02573605 https://hal.archives-ouvertes.fr/hal-02573605/document https://hal.archives-ouvertes.fr/hal-02573605/file/article.pdf https://doi.org/10.4230/LIPIcs.FSCD.2020 |
op_coverage |
Paris, France |
long_lat |
ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
geographic |
Lambda |
geographic_facet |
Lambda |
genre |
Beluga Beluga* |
genre_facet |
Beluga Beluga* |
op_source |
FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction https://hal.archives-ouvertes.fr/hal-02573605 FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. ⟨10.4230/LIPIcs.FSCD.2020⟩ |
op_relation |
info:eu-repo/semantics/altIdentifier/doi/10.4230/LIPIcs.FSCD.2020 hal-02573605 https://hal.archives-ouvertes.fr/hal-02573605 https://hal.archives-ouvertes.fr/hal-02573605/document https://hal.archives-ouvertes.fr/hal-02573605/file/article.pdf doi:10.4230/LIPIcs.FSCD.2020 |
op_rights |
info:eu-repo/semantics/OpenAccess |
op_doi |
https://doi.org/10.4230/LIPIcs.FSCD.2020 |
_version_ |
1766374822846136320 |
spelling |
ftccsdartic:oai:HAL:hal-02573605v1 2023-05-15T15:41:57+02:00 A Type Checker for a Logical Framework with Union and Intersection Types Stolze, Claude Liquori, Luigi Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)) Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP) Logical Time for Formal Embedded System Design (KAIROS) COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED) Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S) Université Nice Sophia Antipolis (. - 2019) (UNS) COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (. - 2019) (UNS) COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S) COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Inria Sophia Antipolis - Méditerranée (CRISAM) Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) Paris, France 2020-06-29 https://hal.archives-ouvertes.fr/hal-02573605 https://hal.archives-ouvertes.fr/hal-02573605/document https://hal.archives-ouvertes.fr/hal-02573605/file/article.pdf https://doi.org/10.4230/LIPIcs.FSCD.2020 en eng HAL CCSD info:eu-repo/semantics/altIdentifier/doi/10.4230/LIPIcs.FSCD.2020 hal-02573605 https://hal.archives-ouvertes.fr/hal-02573605 https://hal.archives-ouvertes.fr/hal-02573605/document https://hal.archives-ouvertes.fr/hal-02573605/file/article.pdf doi:10.4230/LIPIcs.FSCD.2020 info:eu-repo/semantics/OpenAccess FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction https://hal.archives-ouvertes.fr/hal-02573605 FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. ⟨10.4230/LIPIcs.FSCD.2020⟩ 2012 ACM Subject Classification Theory of computation → Lambda calculus Theory of computation → Proof theory Keywords and phrases Intersection types Union types Dependent types Subtyping Type checker Refiner ∆-Framework [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL] [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] info:eu-repo/semantics/conferenceObject Conference papers 2020 ftccsdartic https://doi.org/10.4230/LIPIcs.FSCD.2020 2021-12-12T01:44:18Z International audience We present the syntax, semantics, typing, subtyping, unification, refinement, and REPL of Bull, a prototype theorem prover based on the ∆-Framework, i.e. a fully-typed Logical Framework à la Edinburgh LF decorated with union and intersection types, as described in previous papers by the authors. Bull also implements a subtyping algorithm for the Type Theory Ξ of Barbanera-Dezani-de'Liguoro. Bull has a command-line interface where the user can declare axioms, terms, and perform computations and some basic terminal-style features like error pretty-printing, subexpressions highlighting, and file loading. Moreover, it can typecheck a proof or normalize it. These terms can be incomplete, therefore the typechecking algorithm uses unification to try to construct the missing subterms. Bull uses the syntax of Berardi's Pure Type Systems to improve the compactness and the modularity of the kernel. Abstract and concrete syntax are mostly aligned and similar to the concrete syntax of Coq. Bull uses a higher-order unification algorithm for terms, while typechecking and partial type inference are done by a bidirectional refinement algorithm, similar to the one found in Matita and Beluga. The refinement can be split into two parts: the essence refinement and the typing refinement. Binders are implemented using commonly-used de Bruijn indices. We have defined a concrete language syntax that will allow user to write ∆-terms. We have defined the reduction rules and an evaluator. We have implemented from scratch a refiner which does partial typechecking and type reconstruction. We have experimented Bull with classical examples of the intersection and union literature, such as the ones formalized by Pfenning with his Refinement Types in LF and by Pierce. We hope that this research vein could be useful to experiment, in a proof theoretical setting, forms of polymorphism alternatives to Girard's parametric one. Conference Object Beluga Beluga* Archive ouverte HAL (Hyper Article en Ligne, CCSD - Centre pour la Communication Scientifique Directe) Lambda ENVELOPE(-62.983,-62.983,-64.300,-64.300) |