Extending higher-order unification to support proof irrelevance

DOI10.1007/10930755_16MaRDI QIDQ3559769zbMATH OpenOpenAlexFDO

Authors Jason Reed

Publication date 7 May 2010

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/10930755_16

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• On the Strength of Proof-Irrelevant Type Theories
• On the strength of proof-irrelevant type theories
• scientific article; zbMATH DE number 1670734
• A proof-irrelevant model of Martin-Löf's logical framework
• Irrelevance in type theory with a heterogeneous equality judgement

Cited in

(1)

• Graded modal dependent type theory

This page was built for publication: Extending higher-order unification to support proof irrelevance

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