Mechanizing metatheory in a logical framework
Mechanizing metatheory in a logical framework
复制标题
在逻辑框架中机械化元理论
DOI：
--
复制
发表时间：
2007
影响因子：
1.1
通讯作者：
Daniel R. Licata
中科院分区：
文献类型：
--
作者：
R. Harper;Daniel R. Licata
LF逻辑框架编纂了一种在独立类型λ演算中表示演绎系统（如编程语言和逻辑）的方法。在这种方法中，系统的句法和演绎装置被编码为相关LF类型的规范形式；一个编码是正确的（充分的）当且仅当它定义了演绎系统的装置和相关规范形式之间的组合双射。给定一个适当的编码，人们可以通过推理相关的LF表示来建立演绎系统的元理论性质。LF逻辑框架的第十二实现是将该方法付诸实践的方便而强大的工具。12既支持演绎系统的表示，也支持关于演绎系统的元定理证明的机械验证。本文的目的是提供LF λ演算的最新概述，充分表示的LF方法，以及机械化元理论的12方法。我们首先定义原始LF语言的一种变体，称为规范LF，其中只允许规范形式（长βη-正规形式）。该变体由从属关系参数化，从而支持对LF表示的模块化推理。然后，我们给出了正则LF中一个简单类型λ-演算的充分表示，既说明了充分性，又作为分析对象。使用这种表示，我们形式化并验证了一些元理论结果的证明，包括保存性、确定性和强化性。每个例子都说明了将LF和12用于形式化元理论的一个重要方面。
Abstract The LF logical framework codifies a methodology for representing deductive systems, such as programming languages and logics, within a dependently typed λ-calculus. In this methodology, the syntactic and deductive apparatus of a system is encoded as the canonical forms of associated LF types; an encoding is correct (adequate) if and only if it defines a compositional bijection between the apparatus of the deductive system and the associated canonical forms. Given an adequate encoding, one may establish metatheoretic properties of a deductive system by reasoning about the associated LF representation. The Twelf implementation of the LF logical framework is a convenient and powerful tool for putting this methodology into practice. Twelf supports both the representation of a deductive system and the mechanical verification of proofs of metatheorems about it. The purpose of this article is to provide an up-to-date overview of the LF λ-calculus, the LF methodology for adequate representation, and the Twelf methodology for mechanizing metatheory. We begin by defining a variant of the original LF language, called Canonical LF, in which only canonical forms (long βη-normal forms) are permitted. This variant is parameterized by a subordination relation, which enables modular reasoning about LF representations. We then give an adequate representation of a simply typed λ-calculus in Canonical LF, both to illustrate adequacy and to serve as an object of analysis. Using this representation, we formalize and verify the proofs of some metatheoretic results, including preservation, determinacy, and strengthening. Each example illustrates a significant aspect of using LF and Twelf for formalized metatheory.
高阶逻辑中的定理证明
DOI：
10.1007/978-3-540-71067-7_8
发表时间：
2008
期刊：
--
影响因子：
--
作者：
Aehlig K
通讯作者：
Aehlig K