Meta-logical Frameworks

元逻辑框架

• 批准号: 9988281
• 负责人: Frank Pfenning
• 金额: $ 29.32万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2000
• 资助国家: 美国
• 起止时间: 2000-09-01 至 2003-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9988281&HistoricalAwards=false
• 关键词: Meta; logical; Frameworks

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.

正式的演绎系统在编程语言和逻辑领域起着核心作用。首先，它们用于以非常高级的抽象（例如类型系统或操作语义）来定义语言及其语义。其次，它们构成了与语言有关的算法（例如，类型推理或解释）的基础。第三，它们为研究编程语言和逻辑的元理论提供了共同的依据（例如，评估中的保存型的型型）。由于作者和其他作者和其他人的规范而言，已经对其规范的一般元语言进行了多种兴趣的推论系统。这些元语言通常被引用为TOAS逻辑框架。当他们重点放置元理论推理时，它们被称为元逻辑框架。拟议工作的主要目的是进一步促进与逻辑无关的，计算机辅助形式的推理和元评估的理论和实践。这是当前NSF赠款CCR-9619584的续签。事先相关工作，建议者和当前赠款的结果包括基于逻辑编程语言精灵的设计和启动，基于1998年9月发布的逻辑Frameworklf，名称为Twelf。广泛的案例研究已确认了两种方法的基础方法的广泛适用性，并扩展到线性型理论。提出的工作的主要重点将是在教育和研究中的应用，以及这些应用所提出的实用性和理论问题。