On Irrelevance and Algorithmic Equality in Predicative Type Theory

Abstract

Dependently typed programs contain an excessive amount of static terms which are necessary to please the type checker but irrelevant for computation. To separate static and dynamic code, several static analyses and type systems have been put forward. We consider Pfenning's type theory with irrelevant quantification which is compatible with a type-based notion of equality that respects eta-laws. We extend Pfenning's theory to universes and large eliminations and develop its meta-theory. Subject reduction, normalization and consistency are obtained by a Kripke model over the typed equality judgement. Finally, a type-directed equality algorithm is described whose completeness is proven by a second Kripke model.

36 pages, superseds the FoSSaCS 2011 paper of the first author, titled "Irrelevance in Type Theory with a Heterogeneous Equality Judgement"

References in corpus (2)

• On the strength of proof-irrelevant type theories
• A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance

Cited by in corpus (10)

• Bidirectional Typing
• Normalisation by Evaluation for Type Theory, in Type Theory
• Formalizing of Category Theory in Agda
• A Reasonably Gradual Type Theory
• A Cubical Language for Bishop Sets
• The Independence of Markov's Principle in Type Theory
• An extensible equality checking algorithm for dependent type theories
• Cocon: Computation in Contextual Type Theory
• A Role for Dependent Types in Haskell (Extended version)
• Multimodal Dependent Type Theory