Document Open Access Logo

A Type Checker for a Logical Framework with Union and Intersection Types (System Description)

Authors Claude Stolze, Luigi Liquori

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.37.pdf
  • Filesize: 0.66 MB
  • 24 pages

Document Identifiers

Author Details

Claude Stolze
  • IRIF, Université de Paris, France
Luigi Liquori
  • Université Côte d'Azur, Nice, France
  • Inria Sophia Antipolis - Méditerranée, France

Funding

Work supported by the COST Action CA15123 EUTYPES “The European research network on types for programming and verification"

Acknowledgements

This work could not be have be done without the many useful discussions with Furio Honsell, Ivan Scagnetto, Ugo de'Liguoro, Daniel Dougherty, and the Anonymous Reviewers.

Cite AsGet BibTex

Claude Stolze and Luigi Liquori. A Type Checker for a Logical Framework with Union and Intersection Types (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 37:1-37:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.37

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Proof theory
Keywords
  • Intersection types
  • Union types
  • Dependent types
  • Subtyping
  • Type checker
  • Refiner
  • Δ-Framework

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. A bi-directional refinement algorithm for the calculus of (co)inductive constructions. Logical Methods in Computer Science, 8(1), 2012. Google Scholar
  2. Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de'Liguoro. Intersection and union types: syntax and semantics. Information and Computation, 119(2):202-230, 1995. Google Scholar
  3. Franco Barbanera and Simone Martini. Proof-functional connectives and realizability. Archive for Mathematical Logic, 33:189-211, 1994. Google Scholar
  4. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931-940, 1983. Google Scholar
  5. Henk Barendregt, Wil Dekkers, and Richard Statman. Lambda calculus with types. Cambridge University Press, 2013. Google Scholar
  6. Stefano Berardi. Type dependence and Constructive Mathematics. PhD thesis, University of Turin, 1990. Google Scholar
  7. Jan Bessai, Jakob Rehof, and Boris Düdder. Fast verified BCD subtyping. In Models, Mindsets, Meta: The What, the How, and the Why Not? - Essays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday, volume 11200 of Lecture Notes in Computer Science, pages 356-371. Springer, 2018. Google Scholar
  8. Olivier Boite. Proof reuse with extended inductive types. In Theorem Proving in Higher Order Logics (TPHOLs), pages 50-65, 2004. Google Scholar
  9. Viviana Bono, Betti Venneri, and Lorenzo Bettini. A typed lambda calculus with intersection types. Theoretical Computer Science, 398(1-3):95-113, 2008. Google Scholar
  10. Beatrice Capitani, Michele Loreti, and Betti Venneri. Hyperformulae, Parallel Deductions and Intersection Types. Electronic Notes in Theoretical Computer Science, 50(2):180-198, 2001. Google Scholar
  11. Joshua E. Caplan and Mehdi T. Harandi. A logical framework for software proof reuse. In Symposium on Software Reusability (SSR), pages 106-113, 1995. Google Scholar
  12. Iliano Cervesato and Frank Pfenning. A linear spine calculus. Journal of Logic and Computation, 13(5):639-688, 2003. Google Scholar
  13. Joëlle Despeyroux, Amy P. Felty, and André Hirschowitz. Higher-order abstract syntax in coq. In Mariangiola Dezani-Ciancaglini and Gordon D. Plotkin, editors, Typed Lambda Calculi and Applications, TLCA, volume 902 of Lecture Notes in Computer Science, pages 124-138. Springer, 1995. Google Scholar
  14. Roberto Di Cosmo. Isomorphisms of types: from λ-calculus to information retrieval and language design. Birkhauser, 1995. Google Scholar
  15. Daniel J. Dougherty, Ugo de'Liguoro, Luigi Liquori, and Claude Stolze. A realizability interpretation for intersection and union types. In Asian Symposium on Programming Languages and Systems (APLAS), volume 10017 of Lecture Notes in Computer Science, pages 187-205. Springer-Verlag, 2016. Google Scholar
  16. Gilles Dowek, Thérèse Hardin, and Claude Kirchner. Higher order unification via explicit substitutions. Information and Computation, 157(1-2):183-235, 2000. Google Scholar
  17. Andrej Dudenhefner, Moritz Martens, and Jakob Rehof. The intersection type unification problem. In Formal Structures for Computation and Deduction (FSCD), pages 19:1-19:16. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2016. Google Scholar
  18. Andrej Dudenhefner and Paweł Urzyczyn. Kripke semantics for intersection formulas. Tenth Workshop on Intersection Types and Related Systems, 2020. Google Scholar
  19. Thomas Ehrhard. Non-idempotent intersection types in logical form. In Foundations of Software Science and Computation Structures (FOSSACS/ETAPS), volume 12077 of Lecture Notes in Computer Science, pages 198-216. Springer, 2020. Google Scholar
  20. Amy Felty and Douglas J. Howe. Generalization and reuse of tactic proofs. In Logic Programming and Automated Reasoning (LPAR), pages 1-15, 1994. Google Scholar
  21. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143-184, 1993. Google Scholar
  22. Robert Harper and Daniel R. Licata. Mechanizing metatheory in a logical framework. Journal of Functional Programming, 17(4-5):613-673, July 2007. Google Scholar
  23. J. Roger Hindley. The simple semantics for Coppo-Dezani-Sallé types. In International Symposium on Programming, pages 212-226, 1982. Google Scholar
  24. Furio Honsell, Marina Lenisa, Luigi Liquori, and Ivan Scagnetto. Implementing Cantor’s paradise. In Asian Symposium on Programming Languages and Systems (APLAS), pages 229-250, 2016. Google Scholar
  25. Furio Honsell, Luigi Liquori, Claude Stolze, and Ivan Scagnetto. The Delta-framework. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 37:1-37:21, 2018. Google Scholar
  26. Gérard Huet. A unification algorithm for typed lambda-calculus. Theoretical Computer Science, 1(1):27-57, 1975. Google Scholar
  27. Luigi Liquori and Claude Stolze. A decidable subtyping logic for intersection and union types. In Topics In Theoretical Computer Science (TTCS), volume 10608 of Lecture Notes in Computer Science, pages 74-90. Springer-Verlag, 2017. Google Scholar
  28. Luigi Liquori and Claude Stolze. The Delta-calculus: Syntax and types. In Formal Structures for Computation and Deduction (FSCD), pages 28:1-28:20. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019. Google Scholar
  29. Edgar G. K. López-Escobar. Proof functional connectives. In Methods in Mathematical Logic, volume 1130 of Lecture Notes in Mathematics, pages 208-221. Springer-Verlag, 1985. Google Scholar
  30. William Lovas and Frank Pfenning. Refinement types for logical frameworks and their interpretation as proof irrelevance. Logical Methods in Computer Science, 6(4), 2010. Google Scholar
  31. David MacQueen, Gordon Plotkin, and Ravi Sethi. An ideal model for recursive polymorphic types. Information and Control, 71(1/2):95-130, 1986. Google Scholar
  32. Robert K. Meyer and Richard Routley. Algebraic analysis of entailment I. Logique et Analyse, 15:407-428, 1972. Google Scholar
  33. Grigori Mints. The completeness of provable realizability. Notre Dame Journal of Formal Logic, 30(3):420-441, 1989. Google Scholar
  34. Alexandre Miquel. The implicit calculus of constructions. In Typed Lambda Calculi and Applications (TLCA), pages 344-359. Springer-Verlag, 2001. Google Scholar
  35. Christine Paulin-Mohring. Inductive definitions in the system coq rules and properties. In Typed Lambda Calculi and Applications (TLCA), pages 328-345. Springer, 1993. Google Scholar
  36. Frank Pfenning. Refinement types for logical frameworks. In TYPES, pages 285-299, 1993. Google Scholar
  37. Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In ACM SIGPLAN Notices, volume 23(7), pages 199-208. ACM, 1988. Google Scholar
  38. Benjamin C. Pierce. Programming with intersection types, union types, and bounded polymorphism. PhD thesis, Technical Report CMU-CS-91-205. Carnegie Mellon University, 1991. Google Scholar
  39. Elaine Pimentel, Simona Ronchi Della Rocca, and Luca Roversi. Intersection types from a proof-theoretic perspective. Fundamenta Informaticae, 121(1-4):253-274, 2012. Google Scholar
  40. Garrel Pottinger. A type assignment for the strongly normalizable λ-terms. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 561-577. Academic Press, 1980. Google Scholar
  41. Jason Reed. Higher-order constraint simplification in dependent type theory. In Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), pages 49-56. ACM, 2009. Google Scholar
  42. Simona Ronchi Della Rocca and Luca Roversi. Intersection logic. In Computer Science Logic (CSL), volume 2142 of Lecture Notes in Computer Science, pages 421-428. Springer-Verlag, 2001. Google Scholar
  43. Claude Stolze. Combining union, intersection and dependent types in an explicitly typed lambda-calculus. PhD thesis, Université Côte d'Azur, Inria, 2019. Google Scholar
  44. Claude Stolze. BULL, 2020. URL: https://github.com/cstolze/Bull.
  45. Claude Stolze, Luigi Liquori, Furio Honsell, and Ivan Scagnetto. Towards a logical framework with intersection and union types. In Logical Frameworks and Meta-languages: Theory and Practice (LFMTP), pages 1-9, 2017. Google Scholar
  46. Pawel Urzyczyn. Type reconstruction in f_omega. Mathematical Structures in Computer Science, 7(4):329-358, 1997. Google Scholar
  47. Betti Venneri. Intersection types as logical formulae. Journal of Logic and Computation, 4(2):109-124, 1994. Google Scholar
  48. Beta Ziliani and Matthieu Sozeau. A unification algorithm for Coq featuring universe polymorphism and overloading. In ACM SIGPLAN Notices, volume 50(9), pages 179-191. ACM, 2015. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact