Irrelevance in type theory with a heterogeneous equality judgement

DOI10.1007/978-3-642-19805-2_5zbMATH Open1326.68076OpenAlexW1515341800MaRDI QIDQ3000599FDOQ3000599

Authors: Andreas Abel 

Publication date: 19 May 2011

Published in: Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-19805-2_5

Recommendations

• On irrelevance and algorithmic equality in predicative type theory
• Irrelevance, heterogeneous equality, and call-by-value dependent type systems
• On the strength of proof-irrelevant type theories
• On the Strength of Proof-Irrelevant Type Theories
• Degrees of relatedness. A unified framework for parametricity, irrelevance, ad hoc polymorphism, intersections, unions and algebra in dependent type theory

zbMATH Keywords

dependent typeslogical relationproof irrelevanceuniversal Kripke modelalgorithmic equalityheterogeneously typed equality

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cited In (4)

• Extending higher-order unification to support proof irrelevance
• On irrelevance and algorithmic equality in predicative type theory
• Undecidability of equality for codata types
• Irrelevance, heterogeneous equality, and call-by-value dependent type systems

Uses Software

• Agda

This page was built for publication: Irrelevance in type theory with a heterogeneous equality judgement

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