Elf: a language for logic definition and verified metaprogramming
Elf: a language for logic definition and verified metaprogramming
复制标题
Elf：一种用于逻辑定义和验证元编程的语言
DOI：
10.1109/lics.1989.39186
复制
发表时间：
1989
期刊：
影响因子：
--
通讯作者：
F. Pfenning
中科院分区：
文献类型：
--
作者：
F. Pfenning
给出了Elf的描述，它是一种独立于任何特定逻辑系统的证明处理环境的元语言。ELF用于元程序，如定理证明器、证明转换器或用于具有复杂类型系统的编程语言的类型推理程序。ELF将逻辑定义(采用爱丁堡逻辑框架的LF风格)与逻辑编程(采用lambda Prolog风格)统一起来。它通过为类型提供操作解释来实现这种统一，这与Prolog给某些公式(Horn子句)提供操作解释的方式非常相似。Elf的新特征包括：(1)Elf搜索过程自动构造能够表示对象逻辑证明的项，因此程序不需要显式地构造它们；(2)元程序关于给定逻辑的部分正确性可以在Elf本身中表示和证明；(3)Elf利用Elliott(1989)的统一算法来求解依赖类型的Lambda演算。
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 lambda 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 lambda -calculus with dependent types.<<ETX>>