Andreas Abel
Abstract
Type theory should be able to handle its own meta-theory, both to justify its foundational claims and to obtain a verified implementation. At the core of a type checker for intensional type theory lies an algorithm to check equality of types, or in other words, to check whether two types are convertible. We have formalized in Agda a practical conversion checking algorithm for a dependent type theory with one universe à la Russell, natural numbers, and η-equality for Π types. We prove the algorithm correct via a Kripke logical relation parameterized by a suitable notion of equivalence of terms. We then instantiate the parameterized fundamental lemma twice: once to obtain canonicity and injectivity of type formers, and once again to prove the completeness of the algorithm. Our proof relies on inductive-recursive definitions, but not on the uniqueness of identity proofs. Thus, it is valid in variants of intensional Martin-Löf Type Theory as long as they support induction-recursion, for instance, Extensional, Observational, or Homotopy Type Theory.
Supplemental Material
- Andreas Abel, Thierry Coquand, and Peter Dybjer. 2007. Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings. IEEE Computer Society Press, 3–12. Google Scholar
Digital Library
- Andreas Abel, Thierry Coquand, and Bassel Mannaa. 2016. On Decidability of Conversion in Type Theory. In 22nd International Conference on Types for Proofs and Programs, TYPES 2016, Novi Sad, Serbia, May 23-26, 2016, Book of Abstracts, Silvia Ghilezan and Jelena Ivetic (Eds.). EasyChair.Google Scholar
- Andreas Abel and Brigitte Pientka. 2016. Well-founded recursion with copatterns and sized types. Journal of Functional Programming 26 (2016), 61. Google ScholarCross Ref
- Andreas Abel and Gabriel Scherer. 2012. On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science 8, 1:29 (2012), 1–36. Google ScholarCross Ref
- AgdaTeam. 2017. The Agda Wiki. http://wiki.portal.chalmers.se/agda/pmwiki.phpGoogle Scholar
- Thorsten Altenkirch and Ambrus Kaposi. 2016. Type theory in type theory using quotient inductive types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, Rastislav Bodík and Rupak Majumdar (Eds.). ACM Press, 18–29. Google ScholarDigital Library
- Thorsten Altenkirch and Ambrus Kaposi. 2017. Normalisation by Evaluation for Type Theory, in Type Theory. Logical Methods in Computer Science 13(4:1) (2017), 1–26. Google ScholarCross Ref
- Bruno Barras. 2010. Sets in Coq, Coq in Sets. Journal of Formalized Reasoning 3, 1 (2010), 29–48. Google ScholarCross Ref
- Thierry Coquand. 1991. An Algorithm for Testing Conversion in Type Theory. In Logical Frameworks, Gérard Huet and Gordon Plotkin (Eds.). Cambridge University Press, 255–279. http://dl.acm.org/citation.cfm?id=120477.120486Google Scholar
- Thierry Coquand and Gérard P. Huet. 1988. The Calculus of Constructions. Information and Computation 76, 2/3 (1988), 95–120. Google ScholarDigital Library
- N. G. de Bruijn. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae 75, 5 (1972), 381–392. Google ScholarCross Ref
- Peter Dybjer. 1995. Internal Type Theory. In Types for Proofs and Programs, International Workshop TYPES’95, Torino, Italy, June 5-8, 1995, Selected Papers (Lecture Notes in Computer Science), Stefano Berardi and Mario Coppo (Eds.), Vol. 1158. Springer, 120–134. Google ScholarCross Ref
- Peter Dybjer. 2000. A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. The Journal of Symbolic Logic 65, 2 (2000), 525–549. Google ScholarCross Ref
- Peter Dybjer and Anton Setzer. 2001. Indexed Induction-Recursion. In Proof Theory in Computer Science, International Seminar, PTCS 2001, Dagstuhl Castle, Germany, October 7-12, 2001, Proceedings (Lecture Notes in Computer Science), Reinhard Kahle, Peter Schroeder-Heister, and Robert F. Stärk (Eds.), Vol. 2183. Springer, 93–113. Google ScholarCross Ref
- Peter Dybjer and Anton Setzer. 2003. Induction-recursion and initial algebras. Annals of Pure and Applied Logic 124, 1-3 (2003), 1–47. Google ScholarCross Ref
- Harvey Friedman. 1975. Equality between functionals. In Logic Colloquium (Lecture Notes in Mathematics), R. Parikh (Ed.), Vol. 453. Springer, 22–37. Google ScholarCross Ref
- Herman Geuvers. 1994. A short and flexible proof of Strong Normalization for the Calculus of Constructions. In Types for Proofs and Programs, International Workshop TYPES’94, Båstad, Sweden, June 6-10, 1994, Selected Papers (Lecture Notes in Computer Science), Peter Dybjer, Bengt Nordström, and Jan M. Smith (Eds.), Vol. 996. Springer, 14–38. Google ScholarCross Ref
- Neil Ghani, Lorenzo Malatesta, and Fredrik Nordvall Forsberg. 2015. Positive Inductive-Recursive Definitions. 11, 1 (2015). Google ScholarCross Ref
- Jean-Yves Girard. 1972. Interprétation fonctionnelle et élimination des coupures dans l’arithmétique d’ordre supérieur. Thèse de Doctorat d’État. Université de Paris VII.Google Scholar
- Healfdene Goguen. 1994. A Typed Operational Semantics for Type Theory. Ph.D. Dissertation. University of Edinburgh. Available as LFCS Report ECS-LFCS-94-304.Google Scholar
- Healfdene Goguen. 2000. A Kripke-Style Model for the Admissibility of Structural Rules. In Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers (Lecture Notes in Computer Science), Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack (Eds.), Vol. 2277. Springer, 112–124. Google ScholarCross Ref
- Robert Harper and Frank Pfenning. 2005. On Equivalence and Canonical Forms in the LF Type Theory. ACM Trans. Comput. Logic 6, 1 (Jan. 2005), 61–101. Google ScholarDigital Library
- John Hughes, Lars Pareto, and Amr Sabry. 1996. Proving the Correctness of Reactive Systems Using Sized Types. In Conference Record of POPL’96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996, Hans-Juergen Boehm and Guy L. Steele Jr. (Eds.). ACM Press, 410–423. Google ScholarDigital Library
- INRIA. 2017. The Coq Proof Assistant Reference Manual (version 8.7 ed.). INRIA. http://coq.inria.fr/Google Scholar
- Per Martin-Löf. 1975. An Intuitionistic Theory of Types: Predicative Part. In Logic Colloquium ‘73, H. E. Rose and J. C. Shepherdson (Eds.). North-Holland, 73–118.Google Scholar
- Jorge Luis Sacchini. 2013. Type-Based Productivity of Stream Definitions in the Calculus of Constructions. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013. IEEE Computer Society Press, 233–242. Google ScholarDigital Library
- Carsten Schürmann and Jeffrey Sarnat. 2008. Structural Logical Relations. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, Frank Pfenning (Ed.). IEEE Computer Society Press, 69–80. Google ScholarDigital Library
- Thomas Streicher. 1993. Investigations into Intensional Type Theory. Habilitation thesis, Ludwig-Maximilians-University Munich.Google Scholar
- Benjamin Werner. 1992. A Normalization Proof for an Impredicative Type System with Large Eliminations over Integers. In Proceedings of the 1992 Workshop on Types for Proofs and Programs, Båstad, Sweden, June 1992, Bengt Nordström, Kent Petersson, and Gordon Plotkin (Eds.). 341–357. http://www.cs.chalmers.se/Cs/Research/Logic/Types/proc92.psGoogle Scholar
- Benjamin Werner. 1994. Une Théorie des Constructiones Inductives. Ph.D. Dissertation. Universite Paris 7.Google Scholar
Index Terms
- Decidability of conversion for type theory in type theory
Recommendations
Type theory in type theory using quotient inductive types
POPL '16We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids ...
Type theory in type theory using quotient inductive types
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesWe present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids ...
Parametric quantifiers for dependent type theory
Polymorphic type systems such as System F enjoy the parametricity property: polymorphic functions cannot inspect their type argument and will therefore apply the same algorithm to any type they are instantiated on. This idea is formalized mathematically ...
Comments