The relevance of proof-irrelevance
- 1 January 1998
- book chapter
- Published by Springer Nature
- p. 755-768
- https://doi.org/10.1007/bfb0055099
Abstract
No abstract availableKeywords
This publication has 16 references indexed in Scilit:
- Modularity of strong normalization in the algebraic-λ-cubeJournal of Functional Programming, 1997
- Abstract data type systemsTheoretical Computer Science, 1997
- A Notion of Classical Pure Type System (Preliminary version)Electronic Notes in Theoretical Computer Science, 1997
- Termination of algebraic type systems: The syntactic approachPublished by Springer Nature ,1997
- A short and flexible proof of strong normalization for the calculus of constructionsLecture Notes in Computer Science, 1995
- Some Extensions of Automath: The AUT-4 FamilyPublished by Elsevier ,1994
- A-translation and looping combinators in pure type systemsJournal of Functional Programming, 1994
- Adding algebraic rewriting to the untyped lambda calculusInformation and Computation, 1992
- Inductively defined types in the Calculus of ConstructionsPublished by Springer Nature ,1990
- The calculus of constructionsInformation and Computation, 1988