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

MaRDI QIDQ3300787FDOQ3300787

Authors: Andreas Abel, Thierry Coquand 

Publication date: 30 July 2020

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

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

zbMATH Keywords

expressivityAllen's relationsinterval based temporal logics

Mathematics Subject Classification ID

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

Cites Work

• The calculus of constructions
• Title not available (Why is that?)
• Constructive mathematics and computer programming
• Title not available (Why is that?)
• Parametricity and variants of Girard's \(J\) operator

Cited In (3)

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

Uses Software

• Automath
• Lean

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)