Abstract

This talk focuses on the specification of and reasoning about formal systems such as type assignment and evaluation semantics in programming languages. I introduce a logic which allows key aspects of such systems, including variable binding structure within the objects they deal with, to be specified directly and which allows reasoning to be performed over these specifications. Many of these reasoning tasks inductively analyze the structure of terms by instantiating bound variables with fresh free variables. I show how this can be captured in a logical setting through a process of moving binding from the term level to the proof level. It is often necessary in reasoning to be able to identify occurrences of variables captured by such proof level binders and to be able to distinguish between variable occurrences governed by different binders. I describe a new logical device that is capable of capturing such rich properties about binding, and I show how this device can naturally encode informal arguments based on free variable occurrences. Stepping back, I show how many similar features of specifications can be abstracted out by using an intermediate specification logic. I briefly describe how this intermediate specification logic can be given an operational semantics so that specifications can be animated automatically, and I explain how the specification logic can be exploited during reasoning to yield many interesting theorems “for free”. Finally, I discuss the implementation of these ideas in the Abella theorem proving system and describe the applications of it that I have explored thus far.