A symmetric Lambda calculus for “classical” program extraction

Abstract

In the present paper we introduce a λ-calculus with symmetric reduction rules and “classical” types, i.e. types corresponding to formulas of classical propositional logic. Strong normalization property is proved to hold for such a calculus. We then extend this calculus in order to get a system equivalent to Peano Arithmetic and show, by means of a theorem on the shape of terms in normal form, how to get recursive functions out of proofs of Π02 formulas, i.e. the ones corresponding to program specifications.