Recursive relational specifications are commonly used to describe the computational structure of formal systems. Recent research in proof theory has identified two features that facilitate direct, logic-based reasoning about such descriptions: the interpretation of atomic judgments through recursive definitions and an encoding of binding constructs via generic judgments. However, logics encompassing these two features do not currently allow for the definition of relations that embody dynamic aspects related to binding, a capability needed in many reasoning tasks. We propose a new relation between terms called nominal abstraction as a means for overcoming this deficiency. We incorporate nominal abstraction into a rich logic also including definitions, generic quantification, induction, and co-induction that we then prove to be consistent. We present examples to show that this logic can provide elegant treatments of binding contexts that appear in many proofs, such as those establishing properties of typing calculi and of arbitrarily cascading substitutions that play a role in reducibility arguments.
Bibliographical noteFunding Information:
We are grateful to Alwen Tiu whose observations with respect to the earlier formulation of our ideas in terms of ∇-quantifiers in the heads of clauses eventually led us to a recasting using the nominal abstraction predicate. Useful comments were also received from David Baelde and the reviewers of an earlier version of this paper and our related LICS’08 paper. This work has been supported by the National Science Foundation Grants CCR-0429572 and CCF-0917140 and by INRIA through the “Equipes Associées” Slimmer. Opinions, findings, and conclusions or recommendations expressed in this papers are those of the authors and do not necessarily reflect the views of the National Science Foundation.
- Generic judgments
- Higher-order abstract syntax
- Proof search
- Reasoning about operational semantics
- λ-Tree syntax