Irrelevance in type theory with a heterogeneous equality judgement

DOI10.1007/978-3-642-19805-2_5MaRDI QIDQ3000599zbMATH OpenOpenAlexFDO

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

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)

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

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

Describes a project that uses

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)