On the Strength of Proof-Irrelevant Type Theories
- 1 January 2006
- book chapter
- Published by Springer Nature
- p. 604-618
- https://doi.org/10.1007/11814771_49
Abstract
No abstract availableKeywords
All Related Versions
This publication has 15 references indexed in Scilit:
- Combining programming with theorem provingPublished by Association for Computing Machinery (ACM) ,2005
- Pure type systems formalizedPublished by Springer Nature ,2005
- Extensional equality in intensional type theoryPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- ECC, an extended calculus of constructionsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- The groupoid model refutes uniqueness of identity proofsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A compiled implementation of strong reductionPublished by Association for Computing Machinery (ACM) ,2002
- Elimination with a MotivePublished by Springer Nature ,2002
- Normalized TypesPublished by Springer Nature ,2001
- Definitions by rewriting in the Calculus of ConstructionsMathematical Structures in Computer Science, 1999
- The relevance of proof-irrelevancePublished by Springer Nature ,1998