Meta-logical Frameworks

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

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.