Practical Program Extraction from Classical Proofs

It is well-known that a constructive proof of a formula F written as a λ-term via Curry-Howard isomorphism, computes a function that witnesses F. Murthy [Murthy, C.R., Classical proofs as programs: How, what and why, Technical Report TR 91-1215, Cornell University, Department of Computer Science (1991)] outlined an extension of this result to classical logic, with the double-negation rule mapped to Felleisen's control operator C [Felleisen, M., D. Friedman, E. Kohlbecker and B. Duba, A syntactic theory of sequential control, Theoretical Computer Science 52 (1987), pp. 205–237]. Since C is similar to call/cc operator in Scheme and SML/NJ, this opens a possibility of extracting programs in these languages from classical proofs. However, even though the basic idea has appeared in the literature, there appears to be little work that uses Griffin's extension of the Curry-Howard isomorphism to extract practical programs in real programming languages.In this article, we fill in missing steps in Murthy's argument and extend his method to encompass more interesting proofs by allowing additional ubiquitous inference rules: equality rules, rules for atomic formulas (such as transitivity of ⩽), and rules for pairs of dual decidable atoms (such as ⩽ and >). We illustrate the usefulness of this extension with a complete example of program extraction.