The Not So Simple Proof-Irrelevant Model of CC
- 15 April 2003
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
- p. 240-258
- https://doi.org/10.1007/3-540-39185-1_14
Abstract
No abstract availableKeywords
This publication has 8 references indexed in Scilit:
- Extensional equality in intensional type theoryPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Domain-free pure type systemsJournal of Functional Programming, 2000
- On Relating Type Theories and Set TheoriesLecture Notes in Computer Science, 1999
- Sets in types, types in setsLecture Notes in Computer Science, 1997
- Proof-irrelevance out of excluded-middle and choice in the calculus of constructionsJournal of Functional Programming, 1996
- Lambda Calculi with TypesPublished by Oxford University Press (OUP) ,1992
- The calculus of constructionsInformation and Computation, 1988
- Polymorphism is not set-theoreticLecture Notes in Computer Science, 1984