Sökning: id:"swepub:oai:research.chalmers.se:fbe4913d-171c-459e-8071-df1f7954660c" >
Decidability of Con...
Decidability of Conversion for Type Theory in Type Theory
-
- Abel, Andreas, 1974 (författare)
- Gothenburg University,Göteborgs universitet,Institutionen för data- och informationsteknik, datavetenskap (GU),Department of Computer Science and Engineering, Computing Science (GU)
-
- Öhman, Joakim (författare)
- Fundacion IMDEA Software
-
- Vezzosi, Andrea, 1986 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
(creator_code:org_t)
- 2017-12-27
- 2018
- Engelska.
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 2:POPL, s. 23:1-23:29
- Relaterad länk:
-
https://research.cha... (primary) (free)
-
visa fler...
-
https://dl.acm.org/d...
-
https://research.cha...
-
https://doi.org/10.1...
-
https://gup.ub.gu.se...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Matematik -- Algebra och logik (hsv//swe)
- NATURAL SCIENCES -- Mathematics -- Algebra and Logic (hsv//eng)
- NATURVETENSKAP -- Matematik -- Geometri (hsv//swe)
- NATURAL SCIENCES -- Mathematics -- Geometry (hsv//eng)
- NATURVETENSKAP -- Matematik -- Matematisk analys (hsv//swe)
- NATURAL SCIENCES -- Mathematics -- Mathematical Analysis (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap -- Programvaruteknik (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Software Engineering (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- Formalization
- Agda
- Logical relations
- Dependent types
Publikations- och innehållstyp
- art (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas