Failure of normalization in impredicative type theory with proof-irrelevant propositional equality

MaRDI QIDQ3300787zbMATH OpenFDO

Authors Andreas Abel, Thierry Coquand

Publication date 30 July 2020

Full work available at URL https://arxiv.org/abs/1911.08174, https://lmcs.episciences.org/6606

zbMATH Keywords

expressivityAllen's relationsinterval based temporal logics

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• On irrelevance and algorithmic equality in predicative type theory
• On the strength of proof-irrelevant type theories
• On the Strength of Proof-Irrelevant Type Theories
• Irrelevance in type theory with a heterogeneous equality judgement

Cites work

• scientific article; zbMATH DE number 3506643 (Why is no real title available?)
• scientific article; zbMATH DE number 3349775 (Why is no real title available?)
• Constructive mathematics and computer programming
• Parametricity and variants of Girard's \(J\) operator
• The calculus of constructions

Cited in

(3)

• Reduction Free Normalisation for a proof irrelevant type of propositions
• Constructing a universe for the setoid model
• Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality

Describes a project that uses

Uses Software

• Lean
• Automath

This page was built for publication: Failure of normalization in impredicative type theory with proof-irrelevant propositional equality

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