Reasoning About Specifications of Computation

项目编号：9912387 PI: Miller， Dale机构：Penn State University， University Park题目：关于计算规范的推理计算系统通常在操作语义方面被赋予其含义，而这些，反过来，可以在基于逻辑或类型系统的元语言中形式化。在这种元语言中指定操作语义允许通过在元语言中进行推理得出关于语义的正式结果：例如，编程语言的类型稳健性可以作为指定类型和求值语义的理论的正式结果派生出来。开发这种推理框架的一个挑战是，当使用高阶抽象语法（一种对对象级抽象和替换的优雅的声明性处理）对语法进行编码时，如何正确处理归纳。目前的归纳推理方法要求使用代数项的一阶技术对语法进行编码，这本身就需要笨拙的编码来进行绑定和替换。将开发一种元逻辑，用于对使用高阶抽象语法编码的判断进行归纳推理：这种元逻辑将是一种允许归纳和定义概念的高阶直觉逻辑的扩展。将开发一个原型系统，实现该逻辑并使用它来对指定的非操作语义的计算进行推理。

Proposal Number: 9912387 PI: Miller, Dale AInstitution: Penn State University, University Park Title: Reasoning about Specifications of Computation Computational systems are often given their meaning in terms ofoperational semantics, and these, in turn, can be formalized inmeta-languages based on logics or type systems. Specifyingoperational semantics in such meta-languages allows formal resultsabout semantics to be derived by reasoning within the meta-language:for example, type soundness for a programming language might bederived as a formal consequence from the theories specifying typingand evaluation semantics. One challenge in developing a framework forsuch reasoning is the proper treatment of induction when higher-orderabstract syntax, an elegant and declarative treatment of object-levelabstraction and substitution, is used to encode syntax. Currentapproaches to inductive reasoning requires that syntax be coded usingthe first-order techniques of algebraic terms, which itself requiresclumsy encodings for binding and substitution. A meta-logic that canbe used to reason inductively about judgments coded using higher-orderabstract syntax will be developed: this meta-logic will be anextension of a higher-order intuitionistic logic that admits inductionand a notion of definition. A prototype system that implements thislogic and uses it to reason about computations specified inoperational semantics will be developed.