Sciweavers

CSL
2007
Springer
13 years 11 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