A Symmetric Lambda Calculus for Classical Program Extraction

We introduce aλ-calculus with symmetric reduction rules and “classical” types, i.e., types corresponding to formulas of classical propositional logic. The strong normalization property is proved to hold for such a calculus, as well as for its extension to a system equivalent to Peano arithmetic. A theorem on the shape of terms in normal form is also proved, making it possible to get recursive functions out of proofs ofΠ⁰₂formulas, i.e., those corresponding to program specifications.