Proof-irrelevance out of excluded-middle and choice in the calculus of constructions
From MaRDI portal
Publication:5687912
DOI10.1017/S0956796800001829zbMath0860.68093OpenAlexW2134765879MaRDI QIDQ5687912
Stefano Berardi, Franco Barbanera
Publication date: 16 December 1996
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0956796800001829
Related Items
Interpreting HOL in the calculus of constructions ⋮ Canonical Big Operators ⋮ Categoricity results and large model constructions for second-order ZF in dependent type theory ⋮ Predicativity and constructive mathematics
Uses Software
Cites Work
