Elf: a language for logic definition and verified metaprogramming

A description is given of Elf, a metalanguage for proof manipulation environments that are independent of any particular logical system. Elf is intended for metaprograms such as theorem provers, proof transformers, or type inference programs for programming languages with complex type systems. Elf unifies logic definition (in the style of LF, the Edinburgh logical framework) with logic programming (in the style of λProlog). It achieves this unification by giving types an operational interpretation, much the same way that Prolog gives certain formulas (Horn clauses) an operational interpretation. Novel features of Elf include: (1) the Elf search process automatically constructs terms that can represent object-logic proofs, and thus a program need not construct them explicitly; (2) the partial correctness of metaprograms with respect to a given logic can be expressed and proved in Elf itself; and (3) Elf exploits Elliott´s (1989) unification algorithm for a λ-calculus with dependent types