Analysis and Development of Meta-logics and Logical Frameworks

元逻辑和逻辑框架的分析和开发

• 批准号: 9102753
• 负责人: Dale Miller
• 金额: $ 33.09万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Continuing grant
• 财政年份: 1991
• 资助国家: 美国
• 起止时间: 1991-07-01 至 1995-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9102753&HistoricalAwards=false
• 关键词: Analysis; Development; Meta; logics; Logical

Recent developments in meta-logics and logical frameworks have lead to a new notion of syntax appropriate for specifying computations on such data structures as programs, formulas, proofs, types, and lambda- terms. New meta-programming languages and computer systems have already been designed around these new approaches to syntax. Semantics of meta programs seem to be best explained using combinations of proof theoretic concepts, Kripke models, realizability, and logical relations. This award supports further research into intuitutionistic, constructive, and linear logics. Much of this research is inspired by topics in computational logic, logic programming, and meta-programming. Theoretical results of this work will be applied to issues of programming language design so that logical principles of syntax can be made directly accessible to programmers and system builders and to keep a practical and experimental focus to this proposed research.

元逻辑和逻辑框架的最新发展导致了 一种新的语法概念，适用于指定此类 数据结构如程序、公式、证明、类型和lambda- 届 新的元编程语言和计算机系统 已经围绕着这些新的语法方法设计出来了。 Meta程序的语义似乎最好用 证明理论概念的组合，Kripke模型， 可实现性和逻辑关系。 该奖项进一步支持 研究直觉主义、构造性和线性逻辑。 多 这项研究的灵感来自于计算逻辑，逻辑 编程和元编程。 这项工作的理论成果 将应用于编程语言设计的问题， 语法的逻辑原则可以直接访问， 程序员和系统建设者，并保持一个实用， 实验重点是这项研究。