Mathematical Quotients and Quotient Types in Coq
- 15 April 2003
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
Abstract
No abstract availableKeywords
This publication has 3 references indexed in Scilit:
- Proof-irrelevance out of excluded-middle and choice in the calculus of constructionsJournal of Functional Programming, 1996
- Extensions of pure type systemsPublished by Springer Science and Business Media LLC ,1995
- Axiom of Choice and ComplementationProceedings of the American Mathematical Society, 1975