Meta-logical Frameworks

形式演绎系统在编程语言和逻辑领域起着核心作用。首先，它们用于在非常高级的抽象（例如，类型系统或操作语义）上定义语言及其语义。其次，它们构成了实现与语言相关的算法的基础(例如。（类型推断或解释）。第三，它们为编程语言和逻辑的元理论研究提供了一个共同的基础（例如，在求值时类型的保存）。由于对计算机科学和逻辑中各种各样的演绎系统感兴趣，作者和其他人已经研究了它们规范的通用元语言。这些元语言通常被称为逻辑框架。当它们强调元理论推理时，它们被称为元逻辑框架。本研究的主要目标是进一步发展逻辑独立、计算机辅助的形式推理和元推理的理论和实践。这是当前NSF拨款CCR-9619584的更新。申请人先前的相关工作和当前拨款的结果包括基于逻辑框架lf的逻辑编程语言Elf的设计和实现，该语言于1998年9月以twelve的名义发布。广泛的案例研究证实了12的方法论的广泛适用性及其扩展到线性类型理论。在此更新下提出的工作的主要重点将是在教育和研究中的应用，以及这些应用所提出的实践和理论问题。

Formal deductive systems play a central role in the areas of programming languagesand logics. Firstly, they are used to define languages and their semantics at a veryhigh-level of abstraction (e.g., type systems or operational semantics). Secondly,they form the basis for the implementation of algorithms pertaining to languages(e.g., type inference or interpretation). Thirdly, they provide a common basis forthe study of meta-theory of programming languages and logics (e.g., preservation oftypes under evaluation).Motivated by the tremendous variety of deductive systems of interest in com-puter science and logic, general meta-languages for their specification have beeninvestigated by the author and others. These meta-languages are often referred toas logical frameworks. When they emphasis is placed meta-theoretic reasoning theyhave been called meta-logical frameworks. The primary objective of the proposedwork is to further the theory and practice of logic-independent, computer-assistedformal reasoning and meta-reasoning.This is a renewal of the current NSF Grant CCR-9619584. Prior relevant workby the proposer and the results from the current grant include the design and im-plementation of the logic programming language Elf based on the logical frameworkLF, released in September 1998 under the name Twelf. Extensive case studies haveconfirmed the wide range of applicability of the methodology underlying Twelf andits extension to a linear type theory. The primary emphasis of the work proposedunder this renewal will be applications in education and research, and the practicaland theoretical issues suggested by these applications.