Program Extraction in a Logical Framework Setting

. This paper demonstrates a method of extracting programs from formal deductions represented in the Edinburgh Logical Framework, using the Elf programming language. Deductive systems are given for the extraction of simple types from formulas of first-order arithmetic and of -calculus terms from natural deduction proofs. These systems are easily encoded in Elf, yielding an implementation of extraction that corresponds to modified realizability. Because extraction is itself implemented as a set of formal deductive systems, some of its correctness properties can be partially represented and mechanically checked in the Elf language. 1 Introduction Research in the development of verified programs through theorem proving has traditionally relied on systems based on a fixed logic or type theory (e.g., [3], [5], [12]). Given the current interest in variations on logics and programming languages for proofs-as-programs (e.g. [14], [15], [21]), a more flexible approach may be useful. As argued in..