Subset Coercions in Coq
- 31 December 2006
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
Abstract
No abstract availableThis publication has 9 references indexed in Scilit:
- On the Strength of Proof-Irrelevant Type TheoriesLecture Notes in Computer Science, 2006
- Pure type systems with judgemental equalityJournal of Functional Programming, 2005
- The view from the leftJournal of Functional Programming, 2004
- Interactive Theorem Proving and Program DevelopmentTexts in Theoretical Computer Science An EATCS Series, 2004
- The Not So Simple Proof-Irrelevant Model of CCLecture Notes in Computer Science, 2003
- Principles and Pragmatics of Subtyping in PVSLecture Notes in Computer Science, 2000
- Cayenne—a language with dependent typesACM SIGPLAN Notices, 1998
- Synthesizing proofs from programs in the Calculus of Inductive ConstructionsLecture Notes in Computer Science, 1995
- The calculus of constructionsInformation and Computation, 1988