arXiv:0804.3914v2 [cs.LO] 3 Jun 2008

Reasoning in Abella about Structural
Operational Semantics Specifications
Andrew Gacek1 Dale Miller2 Gopalan Nadathur1
Abstract
The approach to reasoning about structural operational semantics style specifications supported by the
Abella system is discussed. This approach uses λ-tree syntax to treat object language binding and encodes
binding related properties in generic judgments. Further, object language specifications are embedded
directly into the reasoning framework through recursive definitions. The treatment of binding via generic
judgments implicitly enforces distinctness and atomicity in the names used for bound variables. These
properties must, however, be made explicit in reasoning tasks. This objective can be achieved by allowing
recursive definitions to also specify generic properties of atomic predicates. The utility of these various
logical features in the Abella system is demonstrated through actual reasoning tasks. Brief comparisons
with a few other logic based approaches are also made.

1

Introduction

This paper concerns reasoning about the descriptions of systems that manipulate
formal objects such as programs and their specifications. A common approach to
modelling the dynamic and static semantics of these systems is to use a syntaxdriven rule-based presentation. These presentations can be naturally encoded as
theories within a simple, intuitionistic logic. If the intuitionistic logic supports
λ-terms and the quantification of variables ranging over such terms, then it also
provides a convenient means for capturing binding notions in the syntactic objects
of interest; in particular, it facilitates the use of the λ-tree approach to abstract
syntax. A further benefit to using such a logic to encode semantic specifications is
that an immediate and effective animation of them is provided by logic programming
systems such as λProlog [NM88] and Twelf [PS99].
Given a logic-based specification of a formal system, establishing properties of
the system reduces to answering questions about what is provable in the logic encoding the specification. Different approaches can be adopted for this task. At one
1

Department of Computer Science and Engineering, University of Minnesota, Minneapolis, MN 55455.
INRIA Saclay - Île-de-France & LIX/École polytechnique, Palaiseau, France
3 This work has been supported by INRIA through the “Equipes Associées” Slimmer, and by the NSF Grant
CCR-0429572 which includes funding for 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.
2

c 2008

Published by Elsevier Science B. V.

Gacek, Miller, Nadathur

end, the specification logic can be formalized and reasoned about within a general
purpose theorem-proving framework such as that provided by Coq [BC04] or Isabelle [NPW02]. At the other end, one can develop another logic, often called a
meta-logic, that is explicitly tuned to reasoning about the specification logic. It is
the latter approach that we examine here. In particular, we expose its practical use
within the context of a specific theorem-proving system called Abella [Gac08].
The design of a logic that can act as a powerful and expressive meta-logic has
been the subject of much recent research [BGM+ 07,GMN08,MM02,MT05,Tiu06].
The logics emanating from these studies share a common theme: they all provide
recursive definitions as a means for encoding specification logics and some form of
generic reasoning for modelling binding notions at the meta level. We expose here
an expressive and flexible logic called G within this framework. Abella is based on
G but also provides special support for the ways in which G is intended to be used
in meta-reasoning tasks. Our presentation pays attention to the novel features of
both G and Abella from this perspective. Concreteness is provided by considering
proofs of evaluation, typing, and normalization properties of the λ-calculus.
This paper is organized as follows. The logic G is summarized in Section 2 and
its particular realization in Abella is discussed in Section 3. Section 4 illustrates
the use of Abella in a significant theorem-proving task, that of formalizing a Taitstyle proof of normalizability in the λ-calculus. Section 5 points out limitations of
the currently implemented system. Finally, in Section 6 we compare Abella-style
reasoning with some other approaches to the same kind of reasoning tasks.

2

The Logical Foundation

The logic G [GMN08] which we use to formalize arguments about structural operational semantics is based on an intuitionistic and predicative subset of Church’s
Simple Theory of Types. Terms in G are monomorphically typed and are constructed using abstraction and application from constants and (bound) variables.
The provability relation concerns terms of the distinguished type o that are also
called formulas. Logic is introduced by including special constants representing the
propositional connectives ⊤, ⊥, ∧, ∨, ⊃ and, for every type τ that does not contain o, the constants ∀τ and ∃τ of type (τ → o) → o. The binary propositional
connectives are written as usual in infix form and the expression ∀τ x.B (∃τ x.B) abbreviates the formula ∀τ λx.B (respectively, ∃τ λx.B). Type subscripts are typically
omitted from quantified formulas when their identities do not aid the discussion.
The standard treatment of the universal quantifier accords it an extensional
interpretation. When treating λ-tree syntax it is often necessary to give importance
to the form of the argument for a statement like “B(x) holds for all x” rather than
focusing on whether or not every instance of B(x) is true. The ∇ quantifier [MT05]
is used to encode such generic judgments. Specifically, we include the constants
∇τ of type (τ → o) → o for each type τ (not containing o). As with the other
quantifiers, ∇τ x.B abbreviates ∇τ λx.B.
The F Oλ∆∇ logic [MT05] incorporates ∇ quantification into a sequent calculus
presentation of intuitionistic proof by attaching a local signature to every formula
occurrence in a sequent. We are interested here in considering also proofs that use
2

Gacek, Miller, Nadathur

π.B = π ′ .B ′ id
π
Σ : Γ, B ⊢ B ′

Σ : Γ ⊢ B Σ : B, ∆ ⊢ C
cut
Σ : Γ, ∆ ⊢ C

Σ, K, C ⊢ t : τ Σ : Γ, B[t/x] ⊢ C
∀L
Σ : Γ, ∀τ x.B ⊢ C

Σ, h : Γ ⊢ B[h c̄/x]
∀R, h ∈
/Σ
Σ : Γ ⊢ ∀x.B

Σ : Γ, B[a/x] ⊢ C
Σ : Γ ⊢ B[a/x]
∇L, a ∈
/ supp(B)
∇R, a ∈
/ supp(B)
Σ : Γ, ∇x.B ⊢ C
Σ : Γ ⊢ ∇x.B
Σ, K, C ⊢ t : τ Σ : Γ ⊢ B[t/x]
∃R
Σ : Γ ⊢ ∃τ x.B

Σ, h : Γ, B[h c̄/x] ⊢ C
∃L, h ∈
/Σ
Σ : Γ, ∃x.B ⊢ C

Fig. 1. The core rules of G: the introduction rules for the propositional connectives are not displayed.

induction. In this situation, we are led naturally to including certain structural rules
pertaining to local signatures [Tiu06]. Written at the level of formulas, these are
the ∇-exchange rule ∇x∇y.F ≡ ∇y∇x.F and the ∇-strengthening rule ∇x.F ≡ F ,
provided x is not free in F . If we adopt these rules, we can make all local signatures
equal and hence representable by an (implicit) global binder. We shall refer to
these globally ∇-bound variables as nominal constants. Intuitively, one can think
of nominal constants as denoting arbitrary, unique names. Notice that the exchange
rule requires us to consider atomic judgments as being identical if they differ by only
permutations of nominal constants.
The logic G uses the above treatment of the ∇ quantifier that was first introduced
in the LGω system [Tiu06]. Specifically, an infinite collection of nominal constants
are assumed for each type. The set of all nominal constants is denoted by C. These
constants are distinct from the collection of usual, non-nominal constants denoted
by K. We define the support of a term (or formula) t, written supp(t), as the set of
nominal constants appearing in it. A permutation of nominal constants is a type
preserving bijection π from C to C such that {x | π(x) 6= x} is finite. Permutations
are extended to terms (and formulas), written π.t, as follows:
π.a = π(a), if a ∈ C
π.(λx.M ) = λx.(π.M )

π.c = c if c ∈
/ C is atomic
π.(M N ) = (π.M ) (π.N )

Figure 1 presents a subset of the core rules for G; the standard rules for the
propositional connectives have been omitted for brevity. Sequents in this logic have
the form Σ : Γ ⊢ C where Γ is a set and the signature Σ contains all the free
variables of Γ and C. In the rules, Γ, F denotes Γ ∪ {F }. In the ∇L and ∇R rules,
a denotes a nominal constant of appropriate type. In the ∃L and ∀R rules, c̄ is a
listing of the variables in supp(B) and h c̄ represents the application of h to these
constants; raising is used here to encode the dependency of the quantified variable
on supp(B) [Mil92]. The judgment Σ, K, C ⊢ t : τ that appears in the ∀L and ∃R
rules enforces the requirement that the expression t instantiating the quantifier in
the rule is a well-formed term of type τ constructed from the variables in Σ and the
constants in K ∪ C.
Atomic judgments in G are defined recursively by a set of clauses of the form
∀x̄.(∇z̄.H) , B: here H is an atomic formula all of whose free variables are contained in either x̄ or in z̄ and B is an arbitrary formula all of whose free variables
are also free in ∇z̄.H. The atom H is the head of such a clause and B is its body.
No nominal constant is permitted to appear in either of these formulas. A clause of
3

Gacek, Miller, Nadathur

{Σ′ θ : (π.B ′ )θ, Γ′ θ ⊢ C ′ θ}
defL
Σ : A, Γ ⊢ C

Σ′ : Γ′ ⊢ (π.B ′ )θ
defR
Σ:Γ⊢A

Fig. 2. Rules for definitions

this form provides part of the definition of a relation named by H using B. The ∇
quantifiers over H may be instantiated by distinct nominal constants. The variables
x̄ that are bound by the ∀ quantifiers may be instantiated by terms that depend on
any nominal constant except those chosen for the variables in z̄.
Certain auxiliary notions are needed in formalizing the rules for definitions in
G. A substitution θ is a type-preserving mapping from variables to terms such that
the set {x | xθ 6= x}, the domain of θ, is finite. A substitution is extended to a
function from terms to terms in the usual fashion and we write its application using
a postfix notation. If Γ is a set of formulas then Γθ is the set {Jθ | J ∈ Γ}. If Σ is a
signature then Σθ is the signature that results from removing from Σ the variables
in the domain of θ and adding the variables that are free in the range of θ. Given
a clause ∀x1 , . . . , xn .(∇z̄.H) , B, we define a version of it raised over the nominal
constants ā and away from a signature Σ as
∀h̄.(∇z̄.H[h1 ā/x1 , . . . , hn ā/xn ]) , B[h1 ā/x1 , . . . , hn ā/xn ],
where h1 , . . . , hn are distinct variables of suitable type that do not appear in Σ.
Finally, given the sequent Σ : Γ ⊢ C and the nominal constants c̄ that do not
appear in the support of Γ or C, let σ be any substitution of the form
{h′ c̄/h | h ∈ Σ and h′ is a variable of suitable type that is not in Σ}.
Then we call the sequent Σσ : Γσ ⊢ Cσ a version of Σ : Γ ⊢ C raised over c̄.
The introduction rules for atomic judgments based on definitions are presented
in Figure 2. The defL rule has a set of premises that is generated by considering
each definitional clause of the form ∀x̄.(∇z̄.H) , B in the following fashion. Let c̄
be a list of distinct nominal constants equal in length to z̄ such that none of these
constants appear in the support of Γ, A or C and let Σ′ : A′ , Γ′ ⊢ C ′ denote a version
of the lower sequent raised over c̄. Further, let H ′ and B ′ be obtained by taking the
head and body of a version of the clause being considered raised over ā = supp(A)
and away from Σ′ and applying the substitution [c̄/z̄] to them. Then the set of
premises arising from this clause are obtained by considering all permutations π
of āc̄ and all substitutions θ such that (π.H ′ )θ = A′ θ, with the proviso that the
range of θ may not contain any nominal constants. The defR rule, by contrast, has
exactly one premise that is obtained by using any one definitional clause. B ′ and H ′
are generated from this clause as in the defL case, but π is now taken to be any one
permutation of āc̄ and θ is taken to be any one substitution such that (π.H ′ )θ = A′ ,
again with the proviso that the range of θ may not contain any nominal constants.
Some of the expressiveness arising from the quantificational structure permitted
in definitions in G is demonstrated by the following definitional clauses:
(∇x.name x) , ⊤

∀E.(∇x.fresh x E) , ⊤

The ∇ quantifier in the first clause ensures that name holds only for nominal constants. Similarly, the relative scopes of ∀ and ∇ in the second clause force fresh to
hold only between a nominal constant and a term not containing that constant.
4

Gacek, Miller, Nadathur

When G is used in applications, bound variables in syntactic objects will be represented either explicitly, by term-level, λ-bound variables, or implicitly, by nominal
constants. The equivariance principle for nominal constants realizes alpha convertibility in the latter situation. Encoding bound variables by λ-terms ensures that
substitution is built-in and that dependencies of subterms on bindings is controlled;
specific dependencies can be realized by using the device of raising. Definitions with
∇ in the head allow for a similar control over dependencies pertaining to nominal
constants and raising can be used to similar effect with these as well.
The consistency of G requires some kind of stratification condition to govern the
possible negative uses of predicates in the body of definitions. There are several
choices for such a condition. Rather than picking one in an a priori fashion, we will
note relevant such conditions as needed.
The final capability of interest is induction over natural numbers. These numbers
are encoded in G using the type nt and the constructors z : nt and s : nt → nt.
Use of induction is controlled by the distinguished predicate nat : nt → o which is
treated by specific introduction rules. In particular, the left introduction rule for
nat corresponds to natural number induction.

3

The Architecture of Abella

Abella is an interactive theorem prover for the logic G. The structure of Abella
is influenced considerably by a two-level logic approach to specifying and reasoning about computations. There is a logic—the intuitionistic theory of second-order
hereditary Harrop formulas that we call hH 2 here—that provides a convenient vehicle for formulating structural, rule-based characterizations of a variety of properties
such as evaluation and type assignment. An especially useful feature of such encodings is that derivations within this “specification” logic reflect the structure of
derivations in the object logic. 4 Now, the specification logic can be embedded into
G through the medium of definitions. When used in this manner, G plays the role
of a reasoning or meta logic: formulas in G can be used to encapsulate properties
of derivations in the specification logic and, hence, of computations in the object
logic. By keeping the correspondences simple, reasoning within G can be made to
directly reflect the structure of informal arguments relative to the object logics.
This two-level logic approach was enunciated by McDowell and Miller already
in the context of the logic F Oλ∆IN [MM02]. Abella realizes this idea using a richer
logic that is capable of conveniently encoding more properties of computations.
As a theorem prover, Abella also builds in particular properties arising out of the
encoding of the specification logic. We discuss these aspects in more detail below.
The specification logic
ally recursive definitions:

The formulas of hH 2 are given by the following mutu-

G = A | A ⊃ G | ∀τ x.G | G ∧ G

D = A | G ⊃ D | ∀τ x.D

In these definitions, A denotes an atomic formula and τ ranges over types of order
0 or 1 not containing o. The sequents for which proofs are constructed in hH 2 are
4

Since hH 2 is a subset of λProlog [NM88], it turns out that such specifications can also be compiled and
executed effectively [NM99].

5

Gacek, Miller, Nadathur

x:a∈Γ
Γ⊢x:a

Γ ⊢ m : (a → b) Γ ⊢ n : a
Γ⊢mn:b

Γ, x : a ⊢ r : b
x not in Γ
Γ ⊢ (λx : a.r) : (a → b)

Fig. 3. Rules for relating a λ-term to a simple type

∀m, n, a, b[of m (arr a b) ∧ of n a ⊃ of (app m n) b]
∀r, a, b[∀x[of x a ⊃ of (r x) b] ⊃ of (abs a r) (arr a b)]
Fig. 4. Second-order hereditary Harrop formulas (hH 2 ) encoding simply typing

restricted to the form ∆ −→ G where ∆ is a set of D-formulas and G is a G-formula.
For such sequents, provability in intuitionistic logic is completely characterized by
the more restricted notion of (cut-free) uniform proofs [MNPS91]. In the case of
hH 2 , every sequent in a uniform proof of ∆ −→ G is of the form ∆, L −→ G′ for
some G-formula G′ and for some set of atoms L. Thus, during the search for a proof
of ∆ −→ G, the initial context ∆ is global: changes occur only in the set of atoms
on the left and the goal formula on the right.
We briefly illustrate the ease with which type assignment for the simply typed
λ-calculus can be encoded in hH 2 . There are two classes of objects in this domain:
types and terms. For types we will consider a single base type called i and the arrow
constructor for forming function types. Terms can be variables x, applications (m n)
where m and n are terms, and typed abstractions (λx : a.r) where r is a term and
a is the type of x. The standard rules for assigning types to terms are given in
Figure 3. Object-level untyped λ-terms and simple types can be encoded in a
simply typed (meta-level) λ-calculus as follows. The simple types are built from
the two constructors i and arr and terms are built using the two constructors app
and abs. Here, the constructor abs takes two arguments: one for the type of the
variable being abstracted and the other for the actual abstraction. Terms in the
specification logic contain binding and so there is no need for an explicit constructor
for variables. Thus, the (object-level) term (λf : i → i.(λx : i.(f x))) can be encoded
as the meta-level term abs (arr i i) (λf.abs i (λx.app f x)).
Given this encoding of the untyped λ-calculus and simple types, the inference
rules of Figure 3 can be specified by the hH 2 formulas in Figure 4 involving the
binary predicate of. Note that this specification in hH 2 does not maintain an explicit
context for typing assumptions but uses hypothetical judgments instead. Also, the
explicit side-condition in the rule for typing abstractions is not needed since it is
captured by the usual proof theory of the universal quantifier in the hH 2 logic.
Encoding specification logic provability in G
The definitional clauses in
Figure 5 encode hH 2 provability in G. In these and other such clauses in this
paper, we use the convention that capitalized variables are implicitly universally
quantified at the head. This encoding of hH 2 provability derives from McDowell
and Miller [MM02]. As described earlier, uniform proofs in hH 2 contain sequents
of the form ∆, L −→ G where ∆ is a fixed set of D-formulas and L is a varying
set of atomic formulas. Our encoding uses the G predicate prog to represent the
D-formulas in ∆: the D formula ∀x̄.[G1 ⊃ · · · ⊃ Gn ⊃ A] is encoded as the clause
∀x̄.prog A (G1 ∧ · · · ∧ Gn ) , ⊤ and ∀x̄.A is encoded by the clause ∀x̄.prog A tt , ⊤.
6

Gacek, Miller, Nadathur

elementN B (B :: L) , ⊤

element(s N ) B (C :: L) , elementN B L

member B L , ∃n.nat n ∧ elementn B L
seqN L hAi , member A L
seq(s N ) L (B ∧ C) , seqN L B ∧ seqN L C
seq(s N ) L (A ⊃ B) , seqN (A :: L) B
seq(s N ) L (∀B) , ∇x.seqN L (B x)
seq(s N ) L hAi , ∃b.prog A b ∧ seqN L b
seq(s N ) L hAi , prog A tt
Fig. 5. Second-order hereditary Harrop logic in G

Sequents are encoded using the atomic formula (seqN L G) where L is a list encoding
the set of atomic formulas L and G encodes the G-formula. The argument N ,
written as a subscript, encodes the height of the proof tree that is needed in inductive
arguments. The constructor h·i is used to inject the special type of atom into
formulas. To simplify notation, we write L G for ∃n.nat n ∧ seqn L G. When L is
nil we write simply G.
Proofs of universally quantified G formulas in hH 2 are generic in nature. A
natural encoding of this (object-level) quantifier in the definition of seq uses a (metalevel) ∇-quantifier. In the case of proving an implication, the atomic assumption
is maintained in a list (the second argument of seq). The penultimate clause for
seq implements backchaining over a fixed hH 2 specification (stored as prog atomic
formulas). The matching of atomic judgments to heads of clauses is handled by
the treatment of definitions in the logic G, thus the penultimate rule for seq simply
performs this matching and makes a recursive call on the corresponding clause body.
With this kind of an encoding, we can now formulate and prove in G statements
about what is or is not provable in hH 2 . Induction over the height of derivations
may be needed in such arguments and this can be realized via natural number
induction on n in seqn L P . Furthermore, the defL rule encodes case analysis in the
derivation of an atomic goal, leading eventually to a consideration of the different
ways in which an atomic judgment may have been inferred in the specification logic.
Abella is designed to hide much of the details of how the seq and prog specifications
work and to reflect instead the aggregate structure described here.
Since we have encoded the entire specification logic, we can prove general properties about it in G that can then be used in reasoning about particular specifications.
In Abella, various such specification logic properties can be invoked either automatically or through the use of tactics. For example, the following property, which is
provable in G, states the judgment ℓ g is not affected by permuting, contracting,
or weakening the context of hypothetical assumptions ℓ.
∀ℓ1 , ℓ2 , g.(ℓ1

g) ∧ (∀e.member e ℓ1 ⊃ member e ℓ2 ) ⊃ (ℓ2 g)

This property can be applied to any specification judgment that uses hypothetical
assumptions. Using it with the encoding of typing judgments for the simply typed
λ-calculus, for example, we easily obtain that permuting, contracting, or weakening
the typing context of a typing judgment does not invalidate that judgment.
Two additional properties of our specification logic which are useful and prov7

Gacek, Miller, Nadathur

able in G are called the instantiation and cut properties. The instantiation property
recovers the notion of universal quantification from our representation of the specification logic ∀ using ∇. The exact property is
∀ℓ, g.(∇x.(ℓ x) (g x)) ⊃ ∀t.(ℓ t) (g t).
Stated another way, although ∇ quantification cannot be replaced by ∀ quantification in general, it can be replaced in this way when dealing with specification
judgments. The cut property allows us to remove hypothetical judgments using a
proof of such judgments. This property is stated as the formula
∀ℓ1 , ℓ2 , a, g.(ℓ1

hai) ∧ (a :: ℓ2 g) ⊃ (ℓ1 , ℓ2 g),

which can be proved in G: here, ℓ1 , ℓ2 denotes the appending of two contexts. As a
concrete example, we can again take our specification of simply typed λ-calculus and
use the instantiation and cut properties to establish a type substitution property,
i.e., if Γ1 , x : a ⊢ m : b and Γ2 ⊢ n : a then Γ1 , Γ2 ⊢ m[x := n] : b.
Encoding properties of specifications in definitions Definitions were used
above to encode the specification logic and also particular specifications in G. There
is another role for definitions in Abella: they can be used also to capture implicit
properties of a specification that are needed in a reasoning task. As an example,
consider the encoding of type assignment. Here, the instances of (seqN L G) that
arise all have L bound to a list of entries of the form (of x t) where x is a nominal
constant that is, moreover, different from all other such constants appearing in L.
Observing these properties is critical to proving the uniqueness of type assignment.
Towards this end, we may define a predicate cntx via the following clauses:
cntx nil , ⊤

(∇x.cntx ((of x T ) :: L)) , cntx L

Reasoning within G, it can now be shown that L in every (seqN L G) atom whose
proof is considered always satisfies the property expressed by cntx and, further, if
L satisfies such a property then the uniqueness of type assignment is guaranteed.
Induction on definitions The logic G supports induction only over natural
numbers. Thus the definitions of element and seq in Figure 5 both make use of
a natural number argument to provide a target for induction. In Abella, such
arguments are unnecessary since the system implicitly assigns such an additional
argument to all definitions. Thus when we refer to induction over a definition we
mean induction on the implicit natural number argument of that definition.

4

Example: Normalizability in the Typed λ-Calculus

In order to illustrate the strengths and weaknesses of Abella, we detail in this
section a proof of normalizability for the call-by-value, simply typed λ-calculus
(sometimes also called “weak normalizability”). We follow here the proof presented
in [Pie02]. Stronger results are possible for the full, simply typed λ-calculus, but
the one at hand suffices to expose the interesting reasoning techniques. The proof
under consideration is based on Tait’s logical relations argument [Tai67] and makes
use of simultaneous substitutions.
Figure 6 contains the specification of call-by-value evaluation and of simple typ8

Gacek, Miller, Nadathur

∀a, r[value (abs a r)]
∀m, n, m′ [step m m′ ⊃ step (app m n) (app m′ n)]
∀m, n, n′ [value m ∧ step n n′ ⊃ step (app m n) (app m n′ )]
∀a, r, m[value m ⊃ step (app (abs a r) m) (r m)]
∀m[steps m m]

∀m, n, p[step m p ∧ steps p n ⊃ steps m n]

type i

∀a, b[type a ∧ type b ⊃ type (arr a b)]

∀a, b, m, n[of m (arr a b) ∧ of n a ⊃ of (app m n) b]
∀a, b, r[type a ∧ ∀x[of x a ⊃ of (r x) b] ⊃ of (abs a r) (arr a b)]
Fig. 6. Specification of simply-typed λ-calculus

ing for the λ-calculus. Values are recognized by the predicate value. Small-step
evaluation is defined by step, and a possibly zero length sequence of small steps is
defined by steps. The predicate type recognizes well-formed types, and of defines
the typing rules of the calculus. A noteworthy aspect of the specification of the
of predicate is that it uses the type predicate to ensure that types mentioned in
abstraction terms are well-formed: a fact used in later arguments.
The goal of this section is to prove weak normalizability, which we can now state
formally in our meta-logic as follows:
∀M, A.( hof M Ai) ⊃ ∃V.( hsteps M V i) ∧ ( hvalue V i).
The rest of this section describes definitions and lemmas necessary to prove this
formula. In general, almost all results in this section have simple proofs based on
induction, case analysis, applying lemmas, and building results from hypotheses.
For such proofs, we will omit the details except to note the inductive argument and
key lemmas used. The full details of this development are available in the software
distribution of Abella.
Evaluation and typing Definitions can be used in Abella to introduce useful
intervening concepts. One such concept is that of halting. We say that a term
M halts if it evaluates to a value in finitely many steps and we define a predicate
capturing this notion as follows:
halts M , ∃V.( hsteps M V i) ∧ ( hvalue V i).
An most important property about halting is that it is invariant under evaluation
steps (both forwards and backwards). Using the abbreviation F ≡ G for (F ⊃
G) ∧ (G ⊃ F ), we can state this property formally as
∀M, N.( hstep M N i) ⊃ (halts M ≡ halts N ).
This result is immediate in the backward direction, i.e., halts N ⊃ halts M . In the
forward direction it requires showing that one step of evaluation is deterministic:
∀M, N, P.( hstep M N i) ∧ ( hstep M P i) ⊃ N = P.
This formula is proved by induction on the height of the derivation of either one of
the judgments involving the step predicate.
A standard result in the λ-calculus, which we will need later, is that one step of
evaluation preserves typing. This is stated formally as
9

Gacek, Miller, Nadathur

∀M, N, A.( hstep M N i) ∧ ( hof M Ai) ⊃ ( hof N Ai).
The proof of this formula uses induction on the height of the derivation of the
judgment involving the step predicate. An interesting case in this proof is when
step M N is step (app (abs B R) P ) (R P ) for some B, R, and P , i.e., when
β-reduction is performed. Deconstructing the typing judgment
( hof (app (abs B R) P ) Ai)
we can deduce that ( hof P Bi) and ((of x B) :: nil hof (R x) Ai) where x is a
nominal constant. Here we use the instantiation property of our specification logic
to replace x with P yielding ((of P B) :: nil hof (R P ) Ai). Next we apply the cut
property of our specification logic to deduce ( hof (R P ) Ai) which is our goal.
Finally, we note that the contexts which are constructed during the proof of a
typing judgment always have the form (of x1 a1 ) :: . . . :: (of xn an ) :: nil where the
xi ’s are distinct nominal constants and the ai ’s are valid types. We introduce the
following formal definition of cntx to exactly describe such contexts:
cntx nil , ⊤

(∇x.cntx ((of x A) :: L)) , ( htype Ai) ∧ cntx L

Note, ∇ in the definition head ensures that the xi ’s are distinct nominal constants.
The logical relation The difficulty with proving weak normalizability directly is
that the halting property is not closed under application, i.e., halts M and halts N
does not imply halts (app M N ). Instead, we must strengthen the halting property
to one which includes a notion of closure under application. We define the logical
relation reduce by induction over the type of a term as follows:
reduce M i
, ( hof M ii) ∧ halts M
reduce M (arr A B) , ( hof M (arr A B)i) ∧ halts M ∧
∀N.(reduce N A ⊃ reduce (app M N ) B)
Note that reduce is defined with a negative use of itself. Such a usage is permitted
in G only if there is a stratification condition that ensures that there are no logical
cycles in the definition. In this case, the condition to use is obvious: the second
argument to reduce decreases in size in the recursive use.
Like halts, the reduce relation is preserved by evaluation:
∀M, N, A.( hstep M N i) ∧ ( hof M Ai) ⊃ (reduce M A ≡ reduce N A).
This formula is proved by induction on the definition of reduce, using the lemmas
that halts is preserved by evaluation and of is preserved by evaluation.
Clearly reduce is closed under application and it implies the halting property,
thus we strengthen our desired weak normalizability result to the following:
∀M, A.( hof M Ai) ⊃ reduce M A.
In order to prove this formula we will have to induct on the height of the proof
of the judgment ( hof M Ai). However, when we consider the case that M is
an abstraction, we will not be able to use the inductive hypothesis on the body of
M since reduce is defined only on closed terms, i.e., those typeable in the empty
context. The standard way to deal with this issue is to generalize the desired formula
to say that if M , a possibly open term, has type A then each closed instantiation
for all the free variables in M , say N , satisfies reduce N A. This requires a formal
10

Gacek, Miller, Nadathur

description of simultaneous substitutions that can “close” a term.
Arbitrary cascading substitutions and freshness Given (L hof M Ai), i.e.,
an open term and its typing context, we define a process of substituting each free
variable in M with a value V which satisfies the logical relation for the appropriate
type. We define this subst relation as follows:
subst nil M M , ⊤
(∇x. subst ((of x A) :: L) (R x) M ) ,
∃V. reduce V A ∧ ( hvalue V i) ∧ subst L (R V ) M
By employing ∇ in the head of the second clause, we are able to use the notion
of substitution in the meta-logic to directly and succinctly encode substitution in
the object language. Also note that we are, in fact, defining a process of cascading
substitutions rather than simultaneous substitutions. Since the substitutions we
define (using closed terms) do not affect each other, these two notions of substitution
are equivalent. We will have to prove some part of this formally, of course, which
in turn requires proving results about the (non)occurrences of nominal constants in
our judgments. The results in this section are often assumed in informal proofs.
One consequence of defining cascading substitutions via the notion of substitution in the meta-logic is that we do not get to specify where substitutions are
applied in a term. In particular, given an abstraction abs A R we cannot preclude
the possibility that a substitution for a nominal constant in this term will affect the
type A. Instead, we must show that well-formed types cannot contain free variables
which can be formalized as ∀A.∇x.( htype (A x)i) ⊃ ∃B. A = λy.B. This formula
essentially states that any well-formed type which possibly depends on a nominal
constant x must depend on it only in a vacuous way.
The above result about types assumes that judgments concerning type occur in
an empty context. Now, such judgments actually enter the picture through uses
of the specification logic rule for of that deals with the case of abstractions. This
means that we have to consider judgments involving type that have a context meant
to be used in judgments involving the of predicate. To use the result we have just
established, we must show that these contexts can be ignored. We formalize this as
∀L, A. cntx L ∧ (L htype Ai) ⊃ ( htype Ai), a formula that can be proved using
induction on the proof of the judgment (L htype Ai). In the base case we must
establish ∀L, A. cntx L ∧ member (type A) L ⊃ ⊥, which is proved by induction on
the proof of member.
Another necessary result is that in any provable judgment of the form (L
hof M Ai), any nominal constant (denoting a free variable) in M must also occur
in L, i.e.,
∀L, R, A.∇x. cntx L ∧ (L hof (R x) (A x)i) ⊃ ∃M. R = λy.M
The proof is by induction on the height of the derivation of the judgment involving
of. In the base case, we need that an element of a list cannot contain any nominal
constant which does not occur in the list, i.e., ∀L, E.∇x. member (E x) L ⊃
∃F. E = λy.F . This formula is proved by induction on member.
We next show that typing judgments produce well-formed types by proving
∀L, M, A. cntx L ∧ (L hof M Ai) ⊃ ( htype Ai).
11

Gacek, Miller, Nadathur

The induction here is on the height of the derivation of the judgment involving of
and the base case is ∀L, M, A. cntx L ∧ member (of M A) L ⊃ ( htype Ai), which
is proved by a simple induction on member.
Given our repertoire of results about the occurrences of nominal constants in
judgments, we can now prove fundamental properties of arbitrary cascading substitutions. The first property states that closed terms, those typeable in the empty
context, are not affected by substitutions, i.e.,
∀L, M, N, A. ( hof M Ai) ∧ subst L M N ⊃ M = N.
The proof here is by induction on subst which corresponds to induction on the
length of the list L. The key step within the proof is using the lemma that any
nominal constant in the judgment ( hof M Ai) must also be contained in the
context of that judgment. Since the context is empty in this case, there are no
nominal constants in M and thus the substitutions from L do not affect it.
We must show that our cascading substitutions act compositionally on terms in
the object λ-calculus. This is stated formally for application as follows:
∀L, M, N, R. cntx L ∧ subst L (app M N ) R ⊃
∃M ′ , N ′ . R = app M ′ N ′ ∧ subst L M M ′ ∧ subst L N N ′ .
This is proved by induction on cntx, which amounts to induction on the length of
the list L. For abstractions we prove the following, also by induction on cntx:
∀L, M, R, A. cntx L ∧ subst L (abs A M ) R ∧ ( htype Ai) ⊃
∃M ′ . R = abs A M ′ ∧ (∀V. reduce V A ∧ ( hvalue V i) ⊃
∇x. subst ((of x A) :: L) (M x) (M ′ V )).
Here we have the additional hypothesis of ( htype Ai) to ensure that the substitutions created from L do not affect A. At one point in this proof we have to show
that the order in which cascading substitutions are applied is irrelevant. The key
to showing this is realizing that all substitutions are for closed terms. Since closed
terms cannot contain any nominal constants, substitutions do not affect each other.
Finally, we must show that cascading substitutions preserve typing. Moreover,
after applying a full cascading substitution for all the free variables in a term, that
term should now be typeable in the empty context:
∀L, M, N, A. cntx L ∧ subst L M N ∧ (L hof M Ai) ⊃ ( hof N Ai).
This formula is proved by induction on cntx and by using the instantiation and cut
properties of our specification logic.
The final result Using cascading substitutions we can now formalize the generalization of weak normalizability that we described earlier: given a (possibly open)
well-typed term, every closed instantiation for it satisfies the logical relation reduce:
∀L, M, N, A. cntx L ∧ (L hof M Ai) ∧ subst L M N ⊃ reduce N A.
The proof of this formula is by induction on the height of the derivation of the
typing judgment (L hof M Ai). The inductive cases are fairly straightforward
using the compositional properties of cascading substitutions and various results
about invariance under evaluation. In the base case, we must prove
∀L, M, N, A. cntx L ∧ member (of M A) L ∧ subst L M N ⊃ reduce N A,
12

Gacek, Miller, Nadathur

which is done by induction on cntx. Weak normalizability is now a simple corollary
where we take L to be nil. Thus we have proved ∀M, A.( hof M Ai) ⊃ halts M .

5

Assessment and Future Work

The Abella system has been tested with several prototypical examples; details are
available with the system distribution. These experiments indicate considerable
promise for the two-level logic based approach in reasoning about formal systems.
However, the experiments have also revealed some issues with Abella at a practical
level. We discuss these below and suggest work aimed at addressing them.
Base case lemmas Every lemma whose proof uses induction on a specification
logic judgment with a non-empty context requires another lemma to be proved
for the base case where that judgment follows because it is in the context. This
creates mundane overhead. The work in these base case lemmas consists of a simple
induction over the length of the context. Support for richer tactics for induction on
specification judgments might lead to more user friendly behavior in such cases.
Types in specifications The specification logic is embedded as an untyped logic
in G. This is usually not an issue: specification logic judgments themselves impose
type restrictions on terms. For example, the typing judgment of M A holds only if
M is a λ-term. However, sometimes explicit type judgments—such as the judgment
type for recognizing well-formed simple types—are required in specifications. One
possibility that is being considered for addressing the typing issue that is of an
implementation such as Abella automatically generating recognizer predicates based
on type information. These predicates could then be implicitly attached to all
declarations of meta-level variables.
Different specification logics Currently, Abella has built into it exactly one
specification language (hH 2 ) and exactly one proof system for it (uniform proofs).
Certain application areas might benefit from having other proof systems for intuitionistic logic available as well as other specification logics. For example, linear logic
specification languages [HM94,Mil96] can be used to provide declarative specifications of the operational semantics of programming languages that contain features
such as references, exceptions, and concurrency. Thus, McDowell and Miller [MM02]
presented a seq-like predicate for a subset of intuitionistic linear logic that they used
to specify the operational semantics of a simple functional language extended with
references and to then prove a subject-reduction theorem for that language. It
would be natural to consider extending the specification logic in Abella to be all
of intuitionistic linear logic (or, in fact, all of linear logic) since this would enhance
that logic’s expressiveness a great deal. Such an extension could be designed so that
if a given specification did not employ the novel linear logic connectives, then the
encoding of seq would modularly revert back to that of intuitionistic logic.

6

Related Work

Nominal logic approach The Nominal package for Isabelle/HOL automates a
process of defining and proving standard results about α-equivalence classes [UT05].
13

Gacek, Miller, Nadathur

This allows for formal reasoning over objects with binding which is close to informal
reasoning. One drawback of the nominal approach is that it does not provide a
notion of substitution, and thus users must define their own substitution function
and prove various properties relating to it. A proof of weak normalizability for the
simply typed λ-calculus has been conducted with the nominal package [NU08], and
in this case a notion of simultaneous substitution is used. For the nominal approach,
this extended notion of substitution can be defined directly since one works with αequivalence classes and not higher-order terms as in our case. Additionally, the cost
of defining and reasoning about simultaneous substitution is not a significant step
up from what is already required for standard substitution in the nominal approach.
The specification language for the nominal package is functions and predicates
over α-equivalence classes. This language does not have a built-in notion of hypothetical judgments which are typically useful for describing structural rules over
objects with binding. For example, by encoding the simply typed λ-calculus in our
specification language using hypothetical judgments for typing assumptions, we derive a type substitutivity property as consequence of general instantiation and cut
properties of the logic, see Section 3. In the nominal approach, such a proof must
be conducted manually.
Twelf The Twelf system [PS99] uses LF terms and types for a specification language [HHP93] and the meta-logic M+
2 [Sch00] for reasoning. The primary difference between the Twelf approach and ours is that the M+
2 meta-logic is relatively
weak in expressive power. For instance, it is restricted to Π2 formulas (i.e., ∀∃
formulas) and lacks logical connectives such as conjunction, disjunction, and implication. Despite these restrictions, the meta-logic is expressive enough for most common reasoning tasks and has been very successful in practice. Another significant
difference is that M+
2 is designed with an inherent notion of a global hypothetical
context. Thus the meta-logic builds in some notion of which judgments can depend
on assumptions of other judgments. This is less of a concern in our approach since
each judgments has its own local context.
Due to the Π2 restriction of the meta-logic M+
2 , it is not possible to encode a
direct proof of weak normalizability for the simply typed λ-calculus using a logical
relations argument. Recently, however, an indirect proof was completed using an
intermediate assertion logic which has enough richness to encode the proper logical
relation [SS08]. This is a useful technique for extending the expressive power of the
Twelf system, but it comes with the cost of moving from a two-level logic approach
to a three-level logic approach.
Locally nameless The locally nameless representation for syntactic objects with
binding is a first-order approach using de Bruijn indices for bound variables and
names for free variables. This balance between two representational techniques
has been used successfully in practice [ACP+ 08]. Our approach to representation
can be seen as a meta-level version of this balance where we use (meta-level) λterms to represent explicitly bound variables and (meta-level) nominal constants
for implicitly bound variables (i.e., free variables). With this understanding, the
trade-off between the first-order and meta-level approaches to bound/free variable
representation is that the former works with existing theorem provers while the
latter has substitution and equivariance built-in.
14

Gacek, Miller, Nadathur

References
[ACP+ 08] Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie
Weirich. Engineering formal metatheory. In 35th ACM Symp. on Principles of Programming
Languages, pages 3–15. ACM, January 2008.
[BC04] Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development.
Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science.
Springer Verlag, 2004.
[BGM+ 07] David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. The Bedwyr
system for model checking over syntactic expressions. In Frank Pfenning, editor, 21th Conference
on Automated Deduction (CADE), number 4603 in LNAI, pages 391–397. Springer, 2007.
[Gac08] Andrew Gacek.
The Abella interactive theorem prover (system description).
In
Fourth International Joint Conference on Automated Reasoning, 2008.
Available from
http://arxiv.org/abs/0803.2305. To appear in IJCAR.
[GMN08] Andrew Gacek, Dale Miller, and Gopalan Nadathur. Combining generic judgments with
recursive definitions. In F. Pfenning, editor, 23th Symp. on Logic in Computer Science. IEEE
Computer Society Press, 2008. To appear.
[HHP93] Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of
the ACM, 40(1):143–184, 1993.
[HM94] Joshua Hodas and Dale Miller. Logic programming in a fragment of intuitionistic linear logic.
Information and Computation, 110(2):327–365, 1994.
[Mil92] Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14(4):321–358,
1992.
[Mil96] Dale Miller. Forum: A multiple-conclusion specification logic. Theoretical Computer Science,
165(1):201–232, September 1996.
[MM02] Raymond McDowell and Dale Miller. Reasoning with higher-order abstract syntax in a logical
framework. ACM Trans. on Computational Logic, 3(1):80–136, 2002.
[MNPS91] Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a
foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.
[MT05] Dale Miller and Alwen Tiu. A proof theory for generic judgments.
Computational Logic, 6(4):749–783, October 2005.

ACM Trans. on

[NM88] Gopalan Nadathur and Dale Miller. An Overview of λProlog. In Fifth International Logic
Programming Conference, pages 810–827, Seattle, August 1988. MIT Press.
[NM99] Gopalan Nadathur and Dustin J. Mitchell. System description: Teyjus — A compiler and
abstract machine based implementation of λProlog. In H. Ganzinger, editor, 16th Conference
on Automated Deduction (CADE), number 1632 in LNAI, pages 287–291, Trento, 1999. Springer.
[NPW02] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant
for Higher-Order Logic. Springer, 2002. LNCS Tutorial 2283.
[NU08] Julien Narboux and Christian Urban. Nominal formalisations of typical SOS proofs. Available
at http://dpt-info.u-strasbg.fr/˜narboux/papers/SOS.pdf, 2008.
[Pie02] Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002.
[PS99] Frank Pfenning and Carsten Schürmann. System description: Twelf — A meta-logical framework
for deductive systems. In H. Ganzinger, editor, 16th Conference on Automated Deduction
(CADE), number 1632 in LNAI, pages 202–206, Trento, 1999. Springer.
[Sch00] Carsten Schürmann. Automating the Meta Theory of Deductive Systems. PhD thesis, Carnegie
Mellon University, October 2000. CMU-CS-00-146.
[SS08] Carsten Schürmann and Jeffrey Sarnat. Structural logical relations. In F. Pfenning, editor, 23th
Symp. on Logic in Computer Science. IEEE Computer Society Press, 2008. To appear.
[Tai67] W. W. Tait. Intensional interpretations of functionals of finite type I. J. of Symbolic Logic,
32(2):198–212, 1967.
[Tiu06] Alwen Tiu. A logic for reasoning about generic judgments. In A. Momigliano and B. Pientka,
editors, Int. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
(LFMTP’06), 2006.
[UT05] Christian Urban and Christine Tasson. Nominal techniques in Isabelle/HOL. In R. Nieuwenhuis,
editor, 20th Conference on Automated Deduction (CADE), volume 3632 of LNCS, pages 38–53.
Springer, 2005.

15

