A Type Checker for a Logical Framework with Union and Intersection Types (System Description)
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. BUL...
Main Authors: | , |
---|---|
Format: | Conference Object |
Language: | English |
Published: |
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
2020
|
Subjects: | |
Online Access: | https://dx.doi.org/10.4230/lipics.fscd.2020.37 https://drops.dagstuhl.de/opus/volltexte/2020/12359/ |
id |
ftdatacite:10.4230/lipics.fscd.2020.37 |
---|---|
record_format |
openpolar |
spelling |
ftdatacite:10.4230/lipics.fscd.2020.37 2023-05-15T15:41:56+02:00 A Type Checker for a Logical Framework with Union and Intersection Types (System Description) Stolze, Claude Liquori, Luigi 2020 application/pdf https://dx.doi.org/10.4230/lipics.fscd.2020.37 https://drops.dagstuhl.de/opus/volltexte/2020/12359/ en eng Schloss Dagstuhl - Leibniz-Zentrum für Informatik https://github.com/cstolze/Bull https://github.com/cstolze/Bull https://dx.doi.org/10.4230/LIPIcs.FSCD.2020 info:eu-repo/semantics/openAccess Creative Commons Attribution 3.0 Unported license https://creativecommons.org/licenses/by/3.0/legalcode CC-BY Intersection types Union types Dependent types Subtyping Type checker Refiner Δ-Framework Theory of computation → Lambda calculus Theory of computation → Proof theory Conference Paper Text article-journal ScholarlyArticle 2020 ftdatacite https://doi.org/10.4230/lipics.fscd.2020.37 https://doi.org/10.4230/LIPIcs.FSCD.2020 2021-11-05T12:55:41Z 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* DataCite Metadata Store (German National Library of Science and Technology) Lambda ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
institution |
Open Polar |
collection |
DataCite Metadata Store (German National Library of Science and Technology) |
op_collection_id |
ftdatacite |
language |
English |
topic |
Intersection types Union types Dependent types Subtyping Type checker Refiner Δ-Framework Theory of computation → Lambda calculus Theory of computation → Proof theory |
spellingShingle |
Intersection types Union types Dependent types Subtyping Type checker Refiner Δ-Framework Theory of computation → Lambda calculus Theory of computation → Proof theory Stolze, Claude Liquori, Luigi A Type Checker for a Logical Framework with Union and Intersection Types (System Description) |
topic_facet |
Intersection types Union types Dependent types Subtyping Type checker Refiner Δ-Framework Theory of computation → Lambda calculus Theory of computation → Proof theory |
description |
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. |
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 (System Description) |
title_short |
A Type Checker for a Logical Framework with Union and Intersection Types (System Description) |
title_full |
A Type Checker for a Logical Framework with Union and Intersection Types (System Description) |
title_fullStr |
A Type Checker for a Logical Framework with Union and Intersection Types (System Description) |
title_full_unstemmed |
A Type Checker for a Logical Framework with Union and Intersection Types (System Description) |
title_sort |
type checker for a logical framework with union and intersection types (system description) |
publisher |
Schloss Dagstuhl - Leibniz-Zentrum für Informatik |
publishDate |
2020 |
url |
https://dx.doi.org/10.4230/lipics.fscd.2020.37 https://drops.dagstuhl.de/opus/volltexte/2020/12359/ |
long_lat |
ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
geographic |
Lambda |
geographic_facet |
Lambda |
genre |
Beluga Beluga* |
genre_facet |
Beluga Beluga* |
op_relation |
https://github.com/cstolze/Bull https://github.com/cstolze/Bull https://dx.doi.org/10.4230/LIPIcs.FSCD.2020 |
op_rights |
info:eu-repo/semantics/openAccess Creative Commons Attribution 3.0 Unported license https://creativecommons.org/licenses/by/3.0/legalcode |
op_rightsnorm |
CC-BY |
op_doi |
https://doi.org/10.4230/lipics.fscd.2020.37 https://doi.org/10.4230/LIPIcs.FSCD.2020 |
_version_ |
1766374812888858624 |