Design, Implementation, & Application of a Framework for the Formalization of Deductive Systems

设计、实施、

• 批准号: 9303383
• 负责人: Frank Pfenning
• 金额: $ 38.82万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1993
• 资助国家: 美国
• 起止时间: 1993-09-01 至 1997-02-28
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9303383&HistoricalAwards=false
• 关键词: Design; Implementation; & Application; Framework

TITLE: Design, Implementation, & Application of a Framework Formal deductive systems play a central role in the areas of programming languages and logics. First, they are used to define languages and their semantics at a very high-level of abstraction (e.g., type systems or operational semantics). Second, they form the basis for the implementation of algorithms pertaining to languages (e.g., type inference or interpretation). Third, they provide a common basis for the study of meta-theory of programming languages and logics (e.g., preservation of types under evaluation). Motivated by the tremendous variety of deductive systems of interest in computer science and logic, general meta-languages for their specification have been investigated. These meta-languages are often referred to as logical frameworks. The objective of this effort is to further the theory and practice of logic-independent, computer-assisted formal reasoning and meta-reasoning. This research addresses definitional, operational, and meta-theoretical aspects of logical frameworks comprising work on further design, implementation, and application of such frameworks.

框架的设计、实现和应用形式演绎系统在编程语言和逻辑领域发挥着核心作用。首先，它们用于在非常高的抽象级别(例如，类型系统或操作语义)定义语言及其语义。其次，它们构成了实现与语言有关的算法的基础(例如，类型推理或解释)。第三，它们为程序设计语言和逻辑的元理论研究提供了共同的基础(例如，被评估的类型的保存)。在计算机科学和逻辑学中各种感兴趣的演绎系统的推动下，人们研究了用于说明它们的通用元语言。这些元语言通常被称为逻辑框架。这项工作的目的是促进独立于逻辑的、计算机辅助的形式推理和元推理的理论和实践。这项研究涉及逻辑框架的定义、操作和元理论方面，包括进一步设计、实现和应用此类框架的工作。