# Reasoning about higher-order relational specifications

## Y. Wang, K. Chaudhuri, A. Gacek, G. Nadathur

### The 15th Symposium on Principles and Practice of Declarative Programming (PPDP), 2013

The logic of hereditary Harrop formulas (HH) has proven useful for
specifying a wide range of formal systems. This logic includes a form
of hypothetical judgment that leads to dynamically changing sets of
assumptions and that is key to encoding side conditions and contexts
that occur frequently in structural operational semantics (SOS) style
presentations. Specifications are often useful in reasoning about the
systems they describe. The Abella theorem prover supports such
reasoning by explicitly embedding the specification logic within a
rich reasoning logic; specifications are then reasoned about through
this embedding. However, realizing an induction principle in the face
of dynamically changing assumption sets is nontrivial and the original
Abella system uses only a subset of the HH specification logic for
this reason. We develop a method here for supporting inductive
reasoning over all of HH. Our approach takes advantage of a focusing
property of HH to isolate the use of an assumption and the ability to
finitely characterize the structure of any such assumption in the
reasoning logic. We demonstrate the effectiveness of these ideas via
several specification and meta-theoretic reasoning examples that have
been implemented in an extended version of Abella.