research-article

Open access

Decidability of conversion for type theory in type theory

Authors:

Andrea VezzosiAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 2, Issue POPL

Article No.: 23, Pages 1 - 29

https://doi.org/10.1145/3158111

Published: 27 December 2017 Publication History

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.

Supplementary Material

WEBM File (typetheoryintypetheory.webm)

Download
111.96 MB

References

[1]

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.

Digital Library

[2]

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.

[3]

Andreas Abel and Brigitte Pientka. 2016. Well-founded recursion with copatterns and sized types. Journal of Functional Programming 26 (2016), 61.

[4]

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.

[5]

AgdaTeam. 2017. The Agda Wiki. http://wiki.portal.chalmers.se/agda/pmwiki.php

[6]

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.

Digital Library

[7]

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.

[8]

Bruno Barras. 2010. Sets in Coq, Coq in Sets. Journal of Formalized Reasoning 3, 1 (2010), 29–48.

[9]

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.120486

[10]

Thierry Coquand and Gérard P. Huet. 1988. The Calculus of Constructions. Information and Computation 76, 2/3 (1988), 95–120.

Digital Library

[11]

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.

[12]

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.

[13]

Peter Dybjer. 2000. A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. The Journal of Symbolic Logic 65, 2 (2000), 525–549.

[14]

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.

[15]

Peter Dybjer and Anton Setzer. 2003. Induction-recursion and initial algebras. Annals of Pure and Applied Logic 124, 1-3 (2003), 1–47.

[16]

Harvey Friedman. 1975. Equality between functionals. In Logic Colloquium (Lecture Notes in Mathematics), R. Parikh (Ed.), Vol. 453. Springer, 22–37.

[17]

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.

[18]

Neil Ghani, Lorenzo Malatesta, and Fredrik Nordvall Forsberg. 2015. Positive Inductive-Recursive Definitions. 11, 1 (2015).

[19]

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.

[20]

Healfdene Goguen. 1994. A Typed Operational Semantics for Type Theory. Ph.D. Dissertation. University of Edinburgh. Available as LFCS Report ECS-LFCS-94-304.

[21]

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.

[22]

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.

Digital Library

[23]

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.

Digital Library

[24]

INRIA. 2017. The Coq Proof Assistant Reference Manual (version 8.7 ed.). INRIA. http://coq.inria.fr/

[25]

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.

[26]

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.

Digital Library

[27]

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.

Digital Library

[28]

Thomas Streicher. 1993. Investigations into Intensional Type Theory. Habilitation thesis, Ludwig-Maximilians-University Munich.

[29]

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.ps

[30]

Benjamin Werner. 1994. Une Théorie des Constructiones Inductives. Ph.D. Dissertation. Universite Paris 7.

Cited By

Saffrich HThiemann PWeidner MAlves SCockx J(2024)Intrinsically Typed Syntax, a Logical Relation, and the Scourge of the Transfer LemmaProceedings of the 9th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3678000.3678201(2-15)Online publication date: 28-Aug-2024
https://dl.acm.org/doi/10.1145/3678000.3678201
Cohen LForster YKirst DDa Rocha Paiva BRahli VSobocinski PLago UEsparza J(2024)Separating Markov's PrinciplesProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662104(1-14)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662104
Pédrot PSobocinski PLago UEsparza J(2024)“Upon This Quote I Will Build My Church Thesis”Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662070(1-12)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662070
Show More Cited By

Index Terms

Decidability of conversion for type theory in type theory
1. Theory of computation
  1. Logic
    1. Proof theory
    2. Type theory

Recommendations

Type theory in type theory using quotient inductive types
POPL '16

We 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 Languages

We 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 2, Issue POPL

January 2018

1961 pages

EISSN:2475-1421

DOI:10.1145/3177123

Issue’s Table of Contents

Copyright © 2017 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 December 2017

Published in PACMPL Volume 2, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Artifacts Evaluated & Functional

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

29
Total Citations
View Citations
1,329
Total Downloads

Downloads (Last 12 months)358
Downloads (Last 6 weeks)84

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Saffrich HThiemann PWeidner MAlves SCockx J(2024)Intrinsically Typed Syntax, a Logical Relation, and the Scourge of the Transfer LemmaProceedings of the 9th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3678000.3678201(2-15)Online publication date: 28-Aug-2024
https://dl.acm.org/doi/10.1145/3678000.3678201
Cohen LForster YKirst DDa Rocha Paiva BRahli VSobocinski PLago UEsparza J(2024)Separating Markov's PrinciplesProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662104(1-14)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662104
Pédrot PSobocinski PLago UEsparza J(2024)“Upon This Quote I Will Build My Church Thesis”Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662070(1-12)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662070
Liesnikov BCockx J(2024)Building a Correct-by-Construction Type Checker for a Dependently Typed Core LanguageProgramming Languages and Systems10.1007/978-981-97-8943-6_4(63-83)Online publication date: 23-Oct-2024
https://dl.acm.org/doi/10.1007/978-981-97-8943-6_4
Felicissimo T(2024)Generic bidirectional typing for dependent type theoriesProgramming Languages and Systems10.1007/978-3-031-57262-3_6(143-170)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57262-3_6
Laurent TLennon-Bertrand MMaillard K(2024)Artifact DescriptionProgramming Languages and Systems10.1007/978-3-031-57262-3_14(332-337)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57262-3_14
Laurent TLennon-Bertrand MMaillard K(2024)Definitional Functoriality for Dependent (Sub)TypesProgramming Languages and Systems10.1007/978-3-031-57262-3_13(302-331)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57262-3_13
Pujet LTabareau N(2024)Observational Equality Meets CICProgramming Languages and Systems10.1007/978-3-031-57262-3_12(275-301)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57262-3_12
Abel ADanielsson NEriksson O(2023)A Graded Modal Dependent Type Theory with a Universe and Erasure, FormalizedProceedings of the ACM on Programming Languages10.1145/36078627:ICFP(920-954)Online publication date: 30-Aug-2023
https://dl.acm.org/doi/10.1145/3607862
Pujet LTabareau N(2023)Impredicative Observational EqualityProceedings of the ACM on Programming Languages10.1145/35717397:POPL(2171-2196)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571739
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents