Analysis and Development of Meta-logics and Logical Frameworks

元逻辑和逻辑框架的最新发展已经导致了一种新的语法概念，该语法适合于指定对诸如程序、公式、证明、类型和lambda项之类的数据结构的计算。围绕这些新的语法方法，已经设计了新的元编程语言和计算机系统。元程序的语义似乎可以使用证明论概念、克里普克模型、可实现性和逻辑关系的组合得到最好的解释。该奖项支持对直觉主义、建构主义和线性逻辑的进一步研究。这项研究的大部分灵感来自于计算逻辑、逻辑编程和元编程的主题。这项工作的理论结果将被应用于编程语言设计问题，以便程序员和系统构建者能够直接接触到语法的逻辑原理，并保持对拟议研究的实践和实验的关注。

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.