  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.
