Reasoning About Specifications of Computation

Pennsylvania State Univ University Park, University Park PA

Investigators

Abstract

Proposal Number: 9912387 PI: Miller, Dale A Institution: Penn State University, University Park Title: Reasoning about Specifications of Computation Computational systems are often given their meaning in terms of operational semantics, and these, in turn, can be formalized in meta-languages based on logics or type systems. Specifying operational semantics in such meta-languages allows formal results about semantics to be derived by reasoning within the meta-language: for example, type soundness for a programming language might be derived as a formal consequence from the theories specifying typing and evaluation semantics. One challenge in developing a framework for such reasoning is the proper treatment of induction when higher-order abstract syntax, an elegant and declarative treatment of object-level abstraction and substitution, is used to encode syntax. Current approaches to inductive reasoning requires that syntax be coded using the first-order techniques of algebraic terms, which itself requires clumsy encodings for binding and substitution. A meta-logic that can be used to reason inductively about judgments coded using higher-order abstract syntax will be developed: this meta-logic will be an extension of a higher-order intuitionistic logic that admits induction and a notion of definition. A prototype system that implements this logic and uses it to reason about computations specified in operational semantics will be developed.