Canonicity and normalisation for Dependent Type Theory

2018/10/22 by Coquand, Thierry · 3 citations
#FOS: Computer and information sciences #Programming Languages (cs.PL)

paper · doi:10.48550/arxiv.1810.09367

Abstract

We show canonicity and normalization for dependent type theory with a cumulative sequence of universes and a type of Boolean. The argument follows the usual notion of reducibility, going back to Godel's Dialectica interpretation and the work of Tait. A key feature of our approach is the use of a proof relevant notion of reducibility.

Cited by

• Setoids in Intensional Type Theory
• Bidirectional Elaborators à la Carte
• Mechanizing Synthetic Tait Computability in Istari

Related

• Bounded First-Class Universe Levels in Dependent Type Theory
• Computational Higher Type Theory III: Univalent Universes and Exact Equality
• Canonicity and Computability in Homotopy Type Theory
• Algebraic Type Theory and Universe Hierarchies
• Stack Semantics of Type Theory