Meta-logical Frameworks

形式演绎系统在程序设计语言和逻辑领域发挥着核心作用。首先，它们用于在非常高的抽象级别上定义语言及其语义(例如，类型系统或操作语义)。其次，它们构成了实现与语言有关的算法(例如，类型推理或解释)的基础。第三，它们为程序设计语言和逻辑的元理论的研究提供了共同的基础(例如，被评估的类型的保存)。在计算机科学和逻辑中感兴趣的各种演绎系统的推动下，作者和其他人研究了用于说明它们的通用元语言。这些元语言通常被称为逻辑框架。当它们强调元理论推理时，它们就被称为元逻辑框架。这项工作的主要目标是进一步发展与逻辑无关的、计算机辅助的形式推理和元推理的理论和实践。这是对目前美国国家科学基金会授予的CCR-9619584的更新。提出者以前的相关工作和本次赠款的结果包括基于逻辑框架LF的逻辑编程语言ELF的设计和实现，该逻辑框架于1998年9月以Twell f的名称发布。广泛的案例研究证实了支撑Twell f的方法论及其对线性类型理论的扩展具有广泛的适用性。根据这一更新建议的工作的主要重点将是在教育和研究中的应用，以及这些应用所提出的实践和理论问题。

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.