# A two-level logic approach to reasoning about computations

## A. Gacek, D. Miller, G. Nadathur

### Journal of Automated Reasoning 49(2): 241-273 (2012)

Relational descriptions have been used in formalizing diverse
computational notions, including, for example, operational semantics,
typing, and acceptance by non-deterministic machines. We therefore
propose a (restricted) logical theory over relations as a language for
specifying such notions. Our specification logic is further
characterized by an ability to explicitly treat binding in object
languages. Once such a logic is fixed, a natural next question is how
we might prove theorems about specifications written in it. We propose
to use a second logic, called a reasoning logic, for this purpose. A
satisfactory reasoning logic should be able to completely encode the
specification logic. Associated with the specification logic are
various notions of binding: for quantifiers within formulas, for
eigenvariables within sequents, and for abstractions within terms. To
provide a natural treatment of these aspects, the reasoning logic must
encode binding structures as well as their associated notions of
scope, free and bound variables, and capture-avoiding substitution.
Further, to support arguments about provability, the reasoning logic
should possess strong mechanisms for constructing proofs by induction
and co-induction. We provide these capabilities here by using a logic
called G which represents relations over lambda-terms via definitions
of atomic judgments, contains inference rules for induction and
co-induction, and includes a special generic quantifier. We show how
provability in the specification logic can be transparently encoded in
G. We also describe an interactive theorem prover called Abella that
implements G and this two-level logic approach and we present several
examples that demonstrate the efficacy of Abella in reasoning about
computations.