Sciweavers

CSL
2007
Springer
14 years 6 months ago
Classical Program Extraction in the Calculus of Constructions
We show how to extract classical programs expressed in Krivine λc-calculus from proof-terms built in a proof-irrelevant and classical version of the calculus of constructions with...
Alexandre Miquel