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.