Syntactic Theories: Their Automation and Logical Foundation

点击翻译按钮获取中文摘要

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.