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Π 0 2formulas, i. e. , those corresponding to program specifications.

Authors

• Franco Barbanera
• Stefano Berardi

Keywords

No keywords are indexed for this paper.