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 universes. For that, we extend Krivine’s realisability model of classical second-order arithmetic to the calculus of constructions with universes using a structure of Πset which is reminiscent of ω-sets, and show that our realisability model validates Peirce’s law and proof-irrelevance. Finally, we extend the extraction scheme to a primitive data-type of natural numbers in a way which preserves the whole compatibility with the classical realisability interpretation of second-order arithmetic.

• Type: Conference
• Year: 2007
• Where: CSL
• Authors: Alexandre Miquel
• Keywords: Classical Second-order Arithmetic, CSL 2007, Model Validates Peirce, Realisability Model