权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Reasoning About Specifications of Computation

关于计算规范的推理

基本信息

批准号：
9912387
负责人：
Dale Miller
金额：
$ 15.9万
依托单位：
Pennsylvania State Univ University Park
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2000
资助国家：
美国
起止时间：
2000-08-15 至 2003-07-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=9912387&HistoricalAwards=false
关键词：
Reasoning About Specifications Computation

项目摘要

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.

提案编号：9912387 PI：米勒，戴尔A机构：宾夕法尼亚州立大学，大学公园关于计算规范的推理计算系统通常被赋予它们在操作语义方面的意义，而这些又可以在基于逻辑或类型系统的元语言中形式化。在这样的元语言中指定操作语义允许通过元语言中的推理来导出关于语义的正式结果：例如，编程语言的类型可靠性可以作为指定类型和评估语义的理论的正式结果导出。在开发一个框架forsuch推理的一个挑战是正确的处理归纳时，高阶抽象语法，优雅的和声明性的处理对象级抽象和替代，是用来编码语法。目前的归纳推理方法要求语法使用代数项的一阶技术进行编码，这本身就需要笨拙的绑定和替换编码。一个元逻辑，可用于推理归纳使用高阶抽象语法编码的判断将被开发：这个元逻辑将是一个扩展的高阶直觉逻辑，承认归纳和定义的概念。一个原型系统，实现thislogic，并使用它来计算指定inoperational语义的原因将被开发。