Extracting programs from proofs by an extension of the Curry-Howard process

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.