Syntactic Theories: Their Automation and Logical Foundation

俄勒冈州尤金的Zena AriolaU这项建议的总体目标是对编程语言的语义和逻辑基础有一个更稳健的理解。这些活动将基于现实编程语言的句法理论和逻辑的序列演算之间的密切对应。这种对应是Curry-Howard同构的推广，它将简单类型的演算和直观的自然演绎逻辑联系在一起，是许多关于程序的自动推理系统的核心。具体的目标及其潜在的影响是：算法和工具：我们的经验表明，拟议的句法方向和相关逻辑的研究是乏味和容易出错的：它需要重复执行许多平凡但有趣的任务。这样的任务包括验证句法理论是否格式良好，评估是否为定义良好的部分函数，以及主语还原是否成立。在逻辑方面，这些性质关系到逻辑的一致性和证明简化规则的可靠性。因此，为了能够研究非平凡的句法理论和逻辑，研究者以前的工作包括设计和实现适用于句法理论操作自动化的算法和定理证明技术。这项工作已经导致了一个原型系统(SL)，用于关于句法理论的轻量级描述和推理。该提案包括扩展和改进当前原型的活动，并使其可供所有感兴趣的研究人员和学生使用。

ABSTRACT0204389Zena AriolaU of Oregon EugeneThe general objective of this proposal is to gain a more robust understanding of the semantics andlogical foundations of programming languages. The activities will be based on the close correspon-dencebetween syntactic theories for realistic programming languages and sequent calculi for logic.This correspondence is a generalization of the Curry-Howard isomorphism that relates the simplytyped calculus and intuitionistic natural-deduction logic, and is at the heart of many automatedproof systems for reasoning about programs. The specific objectives and their potential impact are:Algorithms and Tools: Our experience has shown that the proposed study of syntactic the-oriesand associated logics is tedious and error-prone: it requires many mundane but fun-damentaltasks to be repeatedly performed. Such tasks include verifying that the syntactic heory is well-formed, that evaluation is a well-defined partial function, and that subject re-duction holds. On the logical side, these properties are related to the consistency of the logic and the soundness of the proof simplication rules. Hence, to enable the study of non-trivial syntactic theories and logics, previous work by the investigators included the design and im-plementation of algorithms and theorem-proving techniques suitable for the automation ofthe manipulation of syntactic theories. This effort has led to a prototype system (SL) for lightweight description and reasoning about syntactic theories. This proposal includes ac-tivities to extend and refine the current prototype and to make it available to all interested researchers and students.