On irrelevance and algorithmic equality in predicative type theory

DOI10.2168/LMCS-8(1:29)2012MaRDI QIDQ2881097zbMATH OpenFDO

Authors Andreas Abel, Gabriel Scherer

Publication date 3 April 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1203.4716

zbMATH Keywords

dependent typeslogical relationproof irrelevancetyped algorithm equalityuniversal Kripke model

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

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.

Recommendations

• Irrelevance in type theory with a heterogeneous equality judgement
• Irrelevance, heterogeneous equality, and call-by-value dependent type systems
• On the Strength of Proof-Irrelevant Type Theories
• A modular type-checking algorithm for type theory with singleton types and proof irrelevance
• A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance

Cited in

(20)

• Canonicity for cubical type theory
• An adequacy theorem for dependent type theory
• scientific article; zbMATH DE number 5173450 (Why is no real title available?)
• Graded modal dependent type theory
• A language with type-dependent equality
• On the strength of proof-irrelevant type theories
• An extensible equality checking algorithm for dependent type theories
• Is Impredicativity Implicitly Implicit
• Irrelevance in type theory with a heterogeneous equality judgement
• Irrelevance, heterogeneous equality, and call-by-value dependent type systems
• A dependent dependency calculus
• On the Strength of Proof-Irrelevant Type Theories
• POPLMark reloaded: mechanizing proofs by logical relations
• scientific article; zbMATH DE number 7566056 (Why is no real title available?)
• Mechanizing proofs with logical relations -- Kripke-style
• Equality, quasi-implicit products, and large eliminations
• Canonicity and normalization for dependent type theory
• \(\eta\)-equivalence in core dependent Haskell
• Multimodal dependent type theory
• Equality checking for general type theories in Andromeda 2

Describes a project that uses

Uses Software

• Agda
• Cayenne
• Coq

This page was built for publication: On irrelevance and algorithmic equality in predicative type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2881097)