Extracting programs from proofs by an extension of the Curry-Howard process
John Newsome Crossley, John C. Shepherdson · Birkhäuser Boston eBooks · 1993
In this paper we provide a general framework for extracting programs from proofs in the language of first order predicate calculus directly, that is to say, without first going through a transformation into second order propositional calculus or other higher order logic. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.