arXiv:cs/0003062v2 [cs.LO] 15 Jan 2001

Reasoning with Higher-Order Abstract Syntax in a
Logical Framework
RAYMOND C. MCDOWELL
Kalamazoo College
and
DALE A. MILLER
Pennsylvania State University

Logical frameworks based on intuitionistic or linear logics with higher-type quantification have
been successfully used to give high-level, modular, and formal specifications of many important
judgments in the area of programming languages and inference systems. Given such specifications,
it is natural to consider proving properties about the specified systems in the framework: for
example, given the specification of evaluation for a functional programming language, prove that
the language is deterministic or that evaluation preserves types. One challenge in developing
a framework for such reasoning is that higher-order abstract syntax (HOAS), an elegant and
declarative treatment of object-level abstraction and substitution, is difficult to treat in proofs
involving induction. In this paper, we present a meta-logic that can be used to reason about
judgments coded using HOAS; this meta-logic is an extension of a simple intuitionistic logic that
admits higher-order quantification over simply typed λ-terms (key ingredients for HOAS) as well
as induction and a notion of definition. The latter concept of definition is a proof-theoretic device
that allows certain theories to be treated as “closed” or as defining fixed points. We explore
the difficulties of formal meta-theoretic analysis of HOAS encodings by considering encodings of
intuitionistic and linear logics, and formally derive the admissibility of cut for important subsets
of these logics. We then propose an approach to avoid the apparent tradeoff between the benefits
of higher-order abstract syntax and the ability to analyze the resulting encodings. We illustrate
this approach through examples involving the simple functional and imperative programming
languages PCF and PCF:= . We formally derive such properties as unicity of typing, subject
reduction, determinacy of evaluation, and the equivalence of transition semantics and natural
semantics presentations of evaluation.
Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions
and Theory—Semantics; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs—Specification Techniques; D.2.4 [Software Engineering]:
Software/Program Verification—Formal Methods; F.4.1 [Mathematical Logic and Formal
Languages]: Mathematical Logic—Mechanical Theorem Proving
General Terms: Languages, Theory, Verification
Additional Key Words and Phrases: definitions, higher-order abstract syntax, induction, logical
frameworks
Authors’ addresses: Raymond C. McDowell, Department of Mathematics and Computer Science,
Kalamazoo College, 1200 Academy Street, Kalamazoo, MI 49006-3295 USA. Dale A. Miller, Department of Computer Science and Engineering, 220 Pond Laboratory, The Pennsylvania State
University, University Park, PA 16802-6106 USA.
The authors have been funded in part by the grants ONR N00014-93-1-1324, NSF CCR-92-09224,
NSF CCR-94-00907, NSF CCR-98-03971, and ARO DAAH04-95-1-0092.
Permission to make digital/hard copy of all or part of this material without fee for personal
or classroom use provided that the copies are not made or distributed for profit or commercial
advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and
notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish,
to post on servers, or to redistribute to lists requires prior specific permission and/or a fee.
c 20TBD ACM 1529-3785/TBD/TBD $5.00
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD, Pages 1–56.

2

·

R. C. McDowell and D. A. Miller

INTRODUCTION
Meta-logics and type systems have been used to specify the semantics of a wide
range of logics and computation systems [Avron et al. 1992; Chirimar 1995; Felty
1993; Pfenning and Rohwedder 1992]. This is done by making judgments, such
as “the term M denotes a program,” “the program M evaluates to the value V ”,
and “the program M has type T ”, into predicates that can be proved or types for
which inhabitants (proofs) are needed. Since these specification languages often
contain quantification at higher-order types and term structures involving λ-terms,
succinct and elegant specifications can be written using higher-order abstract syntax,
a high-level and declarative treatment of object-level bound variables and objectlevel substitution [Miller and Nadathur 1987; Pfenning and Elliot 1988]. In other
approaches to syntactic representation where bound variables are managed directly
using either names or deBruijn-style numbering, these details must be carefully
addressed and dealt with at most levels of a specification.
Recently, logical specification languages have been used to not only describe how
to perform computations but also describe properties about the encoded computations [Basin and Constable 1993; Magnusson and Nordström 1994; Matthews et al.
1993; VanInwegen 1996]. By proving these properties in a formal framework, we can
benefit from automated proof assistance and gain greater confidence in our results.
However, this work has been done in languages that do not support higher-order
abstract syntax and so has not been able to benefit from this representation technique. As a result, theorems about substitution and bound variables can dominate
the task [VanInwegen 1996]. But meta-theoretic reasoning about systems represented in higher-order abstract syntax has been difficult since the languages and
logics that support this notion of syntax do not provide facilities for the fundamental operations of case analysis and induction. Moreover, higher-order abstract
syntax leads to types and recursive definitions that do not give rise to monotone
inductive operators, making inductive principles difficult to find.
These apparent difficulties can be overcome, and in this paper we present a metalogic in which we can naturally reason about specifications in higher-order abstract
syntax. This meta-logic is a higher-order intuitionistic logic with partial inductive
definitions and natural number induction. Induction on natural numbers allows us
to derive other induction principles via the construction of an appropriate measure.
A partial inductive definition [Hallnäs 1991] is a proof-theoretic formalization that
allows certain theories to be treated as “closed” or as defining fixed points. This
allows us to perform case analyses on the defined judgments. We use this definition
mechanism to specify a small, object-level logic which in turn is used to specify
the computation systems under consideration. In this way, we can talk directly
about the structure of object-logic sequents and their provability. This technique
of representing a logic within a logic is not new (see, for example, Felty and Miller
[1988] and Paulson [1986] for some early references) and corresponds to the structure
of common informal reasoning.
The first part of this paper (Sections 1 and 2) presents the meta-logic F Oλ∆IN
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

·

3

(pronounced “fold-n”). To illustrate the use of F Oλ∆IN , we derive several theorems expressing properties of natural numbers and lists. In Part II (Sections 4, 5,
and 6) we consider encodings of intuitionistic and linear logics in F Oλ∆IN to illustrate some difficulties with reasoning in the specification logic about higher-order
abstract syntax and to also demonstrate some strategies to deal with these difficulties. Unfortunately these strategies involve sacrificing some benefits of higher-order
abstract syntax in order to gain the ability to perform some meta-theoretic analyses. We avoid this tradeoff in Part III (Sections 7, 8, 9, and 10) by taking a different
approach to formal reasoning. The key to this approach is to encode the object
system in a specification logic that is separate from the logic F Oλ∆IN in which we
perform the reasoning; this specification logic is itself specified in F Oλ∆IN . This
separation of the specification logic and the meta-logic allows us to reason formally about specification logic sequents and their derivability, and also reflects the
structure of informal reasoning about higher-order abstract syntax encodings. We
illustrate this approach by considering the static and dynamic semantics of small
functional and imperative programming languages; we are able to derive in F Oλ∆IN
such properties as the unicity of typing, determinacy of semantics, and type preservation (subject reduction). We conclude in Section 11 with a brief discussion of our
accomplishments and possible extensions of this work.
Part I: THE META-LOGIC F Oλ∆IN
In this part we introduce the logic which we call F Oλ∆IN , an acronym for “firstorder logic for λ with definitions and natural numbers.” We present the logic in
the first section, and then proceed in the next with some sample definitions and
propositions. We conclude the part by briefly comparing the strength of F Oλ∆IN
with that of other logical systems.
1. A DESCRIPTION OF THE LOGIC
The basic logic is an intuitionistic version of a subset of Church’s Simple Theory
of Types [Church 1940] in which formulas have the type o. The logical connectives
are ⊥, ⊤, ∧, ∨, ⊃, ∀τ , and ∃τ . The quantification types τ (and thus the types of
variables) are restricted to not contain o. Thus F Oλ∆IN supports quantification
over higher-order (non-predicate) types, a crucial feature for higher-order abstract
syntax, but has a first-order proof theory, since there is no quantification over
predicate types. We will use sequents of the form Γ −→ B, where Γ is a finite
multiset of formulas and B is a single formula. The basic inference rules for the
logic are shown in Table I. In the ∀R and ∃L rules, y is an eigenvariable that is
not free in the lower sequent of the rule.
We introduce the natural numbers via the constants z : nt for zero and s : nt → nt
for successor and the predicate nat : nt → o. The right and left rules for this new
predicate are
Γ −→ nat z
−→ B z

natR

Γ −→ nat I
natR
Γ −→ nat (s I)

B j −→ B (s j) B I, Γ −→ C
natL .
nat I, Γ −→ C

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

4

·

R. C. McDowell and D. A. Miller

Inference rules for the core of F Oλ∆IN

Table I.

⊥, Γ −→ B
B, Γ −→ D
∧L
B ∧ C, Γ −→ D

⊥L

C, Γ −→ D
∧L
B ∧ C, Γ −→ D

Γ −→ ⊤

⊤R

B[t/x], Γ −→ C
∀L
∀x.B, Γ −→ C

Γ −→ B Γ −→ C
∧R
Γ −→ B ∧ C

Γ −→ B[y/x]
∀R
Γ −→ ∀x.B

B, Γ −→ D C, Γ −→ D
∨L
B ∨ C, Γ −→ D

B[y/x], Γ −→ C
∃L
∃x.B, Γ −→ C

Γ −→ B
∨R
Γ −→ B ∨ C

Γ −→ C
∨R
Γ −→ B ∨ C

Γ −→ B C, Γ −→ D
⊃L
B ⊃ C, Γ −→ D

A, Γ −→ A

init, where A is atomic

Γ −→ B[t/x]
∃R
Γ −→ ∃x.B
B, Γ −→ C
⊃R
Γ −→ B ⊃ C
B, B, Γ −→ C
cL
B, Γ −→ C

∆ −→ B B, Γ −→ C
cut
∆, Γ −→ C

In the left rule, the predicate B : nt → o represents the property that is proved
by induction, and j is an eigenvariable that is not free in B. The third premise
of that inference
V rule witnesses the fact that, in general, B will express a property
stronger than ( Γ) ⊃ C. Notice that the first two premises of the natL rule involve
no assumptions other than the induction hypothesis (in the second premise). This
is not
V a restriction on induction since one can choose to do induction on, say,
λw.( Γ) ⊃ B w, which would effectively provide the first two premises with the
assumptions from the multiset Γ.
△
A definitional clause is written ∀x̄[p t̄ = B], where p is a predicate constant, every
free variable of the formula B is also free in at least one term in the list t̄ of terms,
and all variables free in t̄ are contained in the list x̄ of variables. Since all free
variables in p t̄ and B are universally quantified, we often leave these quantifiers
implicit when displaying definitional clauses. The atomic formula p t̄ is called the
△
head of the clause, and the formula B is called the body. The symbol = is used
simply to indicate a definitional clause: it is not a logical connective. A definition
is a (perhaps infinite) set of definitional clauses. The same predicate may occur in
the head of multiple clauses of a definition: it is best to think of a definition as a
mutually recursive definition of the predicates in the heads of the clauses.
We must also restrict the use of implication in the bodies of definitional clauses;
otherwise cut-elimination does not hold [Schroeder-Heister 1992]. Toward that end
we assume that each predicate symbol p in the language has associated with it a
natural number lvl(p), the level of the predicate. We then extend the notion of
level to formulas and derivations. Given a formula B, its level lvl(B) is defined as
follows:
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

(1)
(2)
(3)
(4)
(5)

·

5

lvl(p t̄) = lvl(p)
lvl(⊥) = lvl(⊤) = 0
lvl(B ∧ C) = lvl(B ∨ C) = max(lvl(B), lvl(C))
lvl(B ⊃ C) = max(lvl(B) + 1, lvl(C))
lvl(∀x.B) = lvl(∃x.B) = lvl(B).

Given a derivation Π of Γ −→ B, lvl(Π) = lvl(B). We now require that for every
△
definitional clause ∀x̄[p t̄ = B], lvl(B) ≤ lvl(p t̄).
The inference rules for defined atoms are given relative to some fixed definition.
The right-introduction rule for defined atoms is
Γ −→ Bθ
△
Γ −→ p ū defR, where p ū = (p t̄)θ for some clause ∀x̄.[p t̄ = B] ,
where θ is a substitution of terms for variables. The left rule for defined concepts
uses complete sets of unifiers (CSU):
n
o
△
Bθ, Γθ −→ Cθ | θ ∈ CSU (p ū, p t̄) for some clause ∀x̄.[p t̄ = B]
defL ,
p ū, Γ −→ C
where θ is a substitution of terms for variables, and the variables x̄ are chosen to
be distinct from the variables free in the lower sequent of the rule. (A set S of
unifiers of t and u is complete if for every unifier ρ of t and u there is a unifier
θ ∈ S such that ρ is θ ◦ σ for some substitution σ [Huet 1975].) Specifying a set
of sequents as the premise should be understood to mean that each sequent in the
set is a premise of the rule. The right rule corresponds to the logic programming
△
notion of backchaining if we think of = in definitional clauses as reverse implication.
The left rule is similar to definitional reflection [Schroeder-Heister 1993] (not to be
confused with another notion of reflection often considered between a meta-logic
and object-logic) and to an inference rule used by Girard in his note on fixed points
[Girard 1992]. This particular presentation of the rule is due to Eriksson [Eriksson
1991]. Notice that in the defL rule, the free variables of the conclusion can be
instantiated in the premises.
The number of premises of the defL rule may be either infinite or finite (including
zero). If the formula p ū does not unify with the head of any definitional clause,
then the number of premises will be zero. In this case p ū is an unprovable formula
logically equivalent to ⊥, and defL corresponds to the ⊥L rule. If the formula p ū
does unify with the head of a definitional clause, CSUs may be infinite, as is the case
with unifications involving simply typed λ-terms and variables of functional type
(a.k.a. higher-order unification). Clearly an inference rule with an infinite number
of premises is impossible to automate directly. There are many important situations
where CSUs are not only finite but are also singleton (containing a most general
unifier) whenever terms are unifiable. One such case is, of course, the first-order
case. Another case is when the application of functional variables are restricted
to distinct bound variables in the sense of higher-order pattern unification [Miller
1991]. In this paper, all unification problems will fall into this latter case and,
hence, we can count on the definition left-introduction rule to have a finite (and
small) number of premises.
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

6

·

R. C. McDowell and D. A. Miller

Assuming that a definition is given and fixed, we have the following results.
Proposition 1.1 Cut-Elimination for F Oλ∆IN . If a sequent is derivable in
F Oλ∆IN , then it is derivable without using the cut rule.
Proof. The proofs of Schroeder-Heister [1993] regarding cut-elimination for definitions do not appear to extend to our setting where induction is included. A complete proof of this theorem appears in McDowell [1997] and McDowell and Miller
[2000] and is modeled on proofs by Tait and Martin-Löf that use the technical
notions of normalizability and reducibility.
The following corollary is an immediate consequence of this cut-elimination theorem.
Corollary 1.2 Consistency of F Oλ∆IN . There is no derivation in F Oλ∆IN
of the sequent −→ ⊥.
Although cut-elimination holds for this logic, we do not have the subformula
property since the induction predicate B used in the natL rule is not necessarily a
subformula of the conclusion of that inference rule. In fact, the following inference
rule is derivable from the induction rule:
−→ B B, Γ −→ C .
nat I, Γ −→ C
This inference rule resembles the cut rule except that it requires a nat assumption.
Although we fail to have the subformula property, the cut-elimination theorem still
provides a strong basis for reasoning about proofs in F Oλ∆IN . Also this formulation
of the induction principle is natural and close to the one used in actual mathematical practice: that is, invariants must be, at times, clever inventions that are not
simply rearrangements of subformulas. Any automation of F Oλ∆IN will almost certainly need to be interactive, at least for retrieving instantiations for the induction
predicate B.
2. SOME SIMPLE DEFINITIONS AND PROPOSITIONS
In this section we illustrate the use of the logic F Oλ∆IN with some examples. We
first define some predicates over the natural numbers and reason about them. Then
we introduce a list type and consider predicates for it. As we prove properties
about these types and predicates, we will interleave informal descriptions of the
proofs with their realization as derivations in F Oλ∆IN . The formal derivations are
by nature detailed and low-level, breaking down proof principles into small pieces.
As a result, what can seem obvious or be described informally in a small number
of words may take a number of steps to accomplish in the formal derivation. But it
is exactly this nature that makes formal derivations amenable to automation; tools
such as proof editors and theorem provers can make the construction of formal
derivations more natural as well as more robust.
We will describe derivations in a “bottom-up” manner – that is, we will start with
the sequent we wish to derive, apply a rule with that sequent as the conclusion, and
continue in this manner with the rule premises. Thus unproved premises represent
statements of what remains to be proved to establish the original sequent. Since
the formal (F Oλ∆IN ) derivation is presented in pieces, intermixed with descriptive
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

Table II.

·

7

Definitional clauses for predicates over natural numbers
△

I =I = ⊤

△

sum z J J = nat J
△

sum (s I) J (s K) = sum I J K
△

z < (s J) = nat J
△

(s I) < (s J) = I < J

△

I ≤I = ⊤
△

I ≤J = I<J

text, pieces that occur later in the text will generally be (partial) derivations of
unproved premises from earlier pieces.
2.1 Natural Numbers
As described in Section 1, F Oλ∆IN includes a type nt encoding natural numbers and
a membership predicate nat. We now introduce predicates representing equality,
the less-than relation, the less-than-or-equal-to relation, and the addition function.
The types for these predicates are as follows:
= : nt → nt → o
< : nt → nt → o

sum : nt → nt → nt → o
≤ : nt → nt → o .

The definitional clauses for these predicates are shown in Table II; we shall refer
to this set of clauses as D(nat ). We define two numbers to be equal if they are
unifiable. The clauses for sum indicate that the sum of zero and any other number
J is J, and the sum of (s I) and J is the successor of the sum of I and J. Zero is
less than the successor of any number, and (s I) is less than (s J) whenever I is
less than J. Finally, I ≤ J if I is equal to J or if I is less than J.
We now proceed to reason in the logic F Oλ∆IN about natural numbers and these
predicates over them. As our first example, we derive a case analysis rule for
natural numbers. In general the defL rule is used to formalize case analysis, but
the predicate nat is not a defined predicate, and so the defL rule does not apply
in the case of natural numbers. However, a case analysis may be viewed as an
induction in which we do not use the induction hypothesis in the induction step.
Thus we can derive a case analysis rule for natural numbers from the induction
(natL) rule.
Proposition 2.1. For any formula C : o, predicate B : nt → o, term I : nt,
multiset Γ of formulas, and eigenvariable i : nt such that i is not free in B, the
following rule is derivable in F Oλ∆IN :
−→ B z

nat i −→ B (s i) B I, Γ −→ C
nat I, Γ −→ C

.

Proof. This rule expresses the following idea: we want to show that C follows
from Γ and the fact that I is a natural number. Since I is a natural number, it
must be either zero or the successor of another natural number. Thus if we can
show that B holds for zero and for the successor of any natural number (the first
two premises), then we know that B holds for I. It then remains to show that C
follows from B I and Γ (the third premise).
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

8

·

R. C. McDowell and D. A. Miller

To derive this rule, we assume that we have derivations of the premises and proceed to prove the conclusion. That is, we construct in F Oλ∆IN a partial derivation
of the sequent nat I, Γ −→ C, leaving unproved premises of the form −→ B z,
nat i −→ B (s i), and B I, Γ −→ C. This corresponds to working under the assumption that B holds both for zero and for the successor of any number and that
B I and Γ imply C. We proceed by induction on I, using (λi.nat i ∧ B i) as our
induction predicate. As a result, we must establish three things:
(1) the base case: zero is a natural number and B holds for it;
(2) the induction step: if i is a natural number and B holds for it, then the same
is true for (s i);
(3) the relevance of the induction predicate: if I is a natural number and B holds
for it, then Γ implies C.
This staging of the problem is represented in F Oλ∆IN by applying the natL rule:
−→ nat z ∧ B z

nat i ∧ B i −→ nat (s i) ∧ B (s i) nat I ∧ B I, Γ −→ C
natL .
nat I, Γ −→ C

The three premises to the natL rule correspond to the three proof obligations
enumerated above.
Let us first consider the relevance of the induction predicate. This is clear, since
we are working under the assumption that C follows from B I and Γ. This is
formally represented by the partial derivation
B I, Γ −→ C
∧L .
nat I ∧ B I, Γ −→ C
The base case is also simple: zero is obviously a natural number, and we are
working under the assumption that B holds for zero. This is expressed in F Oλ∆IN
by the partial derivation
−→ nat z natR −→ B z
∧R .
−→ nat z ∧ B z
It remains to prove the induction step. Since i is a natural number, (s i) is
as well. In addition, B holds for (s i) by our working assumption. The formal
representation of this reasoning is
init
nat i −→ nat i
natR
nat i −→ nat (s i)
nat i −→ B (s i)
∧R
nat i −→ nat (s i) ∧ B (s i)
∧L .
nat i ∧ B i −→ nat (s i) ∧ B (s i)
We now use this derived case analysis rule to prove that zero is the smallest
natural number.
Proposition 2.2. The formula ∀i(nat i ⊃ z ≤ i) is derivable in F Oλ∆IN using
the definition D(nat ).
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

·

9

Proof. The proof is a simple case analysis on i. To represent this in F Oλ∆IN ,
we apply the ∀R and ⊃ R rules to get
nat i −→ z ≤ i ,
and then use the derived rule of Proposition 2.1, which yields the three sequents
−→ z ≤ z

nat i′ −→ z ≤ (s i′ )

z ≤ i −→ z ≤ i .

In this case, the third premise is immediate:
z ≤ i −→ z ≤ i

init .

If i is zero, then it is immediate that zero is equal to itself and thus less than or
equal to itself:
⊤R
−→ ⊤
−→ z ≤ z defR .
If i is the successor of some number i′ , then z < (s i′ ) by definition, and so
z ≤ (s i′ ) also by definition. This is represented formally by the derivation
init
nat i′ −→ nat i′
′
′ defR
nat i −→ z < (s i )
defR .
nat i′ −→ z ≤ (s i′ )
It is also possible to derive in F Oλ∆IN a rule for complete induction over the
natural numbers [McDowell 1997].
Proposition 2.3 Complete Induction. For any formula C : o, predicate B :
nt → o, term I : nt, multiset Γ of formulas, and eigenvariable j : nt such that j is
not free in B, the following rule is derivable in F Oλ∆IN using the definition D(nat ):
nat j, ∀k(nat k ⊃ k < j ⊃ B k) −→ B j
nat I, Γ −→ C

B I, Γ −→ C

.

The following proposition presents additional properties of natural numbers that
we have derived in F Oλ∆IN , although we do not show the derivations here.
Proposition 2.4. The following formulas are derivable in F Oλ∆IN using the
definition D(nat ):
∀i(nat (s i) ⊃ nat i)
∀i(nat i ⊃ ∀j(i < j ⊃ nat j))
∀i(nat i ⊃ i < (s i))
∀i(nat i ⊃ ∀j(i < (s j) ⊃ i ≤ j))
∀i(nat i ⊃ ∀j∀k(i < j ⊃ j < k ⊃ i < k))
∀i(nat i ⊃ ∀j(nat j ⊃ ∃k(nat k ∧ i < k ∧ j < k)))
∀i(nat i ⊃ ∀j∀k(sum i (s j) k ⊃ sum (s i) j k))
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

10

·

R. C. McDowell and D. A. Miller

∀i(nat i ⊃ ∀j(nat j ⊃ ∃k(nat k ∧ sum i j k)))
∀i(nat i ⊃ ∀j∀k(nat j ⊃ sum i j k ⊃ i ≤ k))
∀i(nat i ⊃ ∀j∀k(nat j ⊃ sum (s i) j k ⊃ j < k)) .
2.2 Lists
In this section we introduce a type lst for lists over an arbitrary but fixed type
τ . The type has two constructors, nil : lst representing the empty list and the
infix operator :: of type τ → lst → lst that adds an element to the front of a list.
Consider the list predicates
length : lst → nt → o
list : lst → o
element : τ → lst → o ,

split : lst → lst → lst → o
permute : lst → lst → o

whose definitional clauses are shown in Table III; we shall refer to this set of clauses
as D(list (τ )). The predicate length represents the function that returns the length
of its list argument. The length of the empty list is zero, and the length of (X :: L)
is one more than the length of L. The predicate list indicates that its argument
has a finite (natural number) length. We shall find this predicate useful for constructing induction principles over lists. The predicate element indicates that its
first argument is a member of its second argument. X is an element of (Y :: L) if
X and Y are the same or if X is an element of L. The predicate split holds if its
first argument represents a merging of the second and third in which the order of
elements in second and third lists is preserved in the first. The empty list can only
be split into two empty lists. To split (X :: L), we split L and add X to the front
of either of the resulting lists. The predicate permute holds if its two arguments
contain the same elements (including repetitions), though not necessarily in the
same order. The empty list only permutes to itself. A list (X :: L1 ) permutes to L2
if removing X from L2 yields a permutation of L1 .
We now derive an induction rule for lists from the induction rule for natural
numbers (natL) using the length of a list as our measure.
Proposition 2.5. For any formula C : o, predicate B : lst → o, term L : lst,
multiset Γ of formulas, and eigenvariables x : τ and l : lst such that x and l are not
free in B, the following rule is derivable in F Oλ∆IN using the definition D(list (τ )):
−→ B nil

B l −→ B (x :: l) B L, Γ −→ C
list L, Γ −→ C

.

Proof. To derive this rule, we construct a partial derivation of the sequent
list L, Γ −→ C, leaving unproved premises of the form −→ B nil, B l −→ B (x :: l),
and B L, Γ −→ C. This corresponds to proving that C follows from Γ and the fact
that L is a list under the assumptions
—B holds for nil;
—for any x′ and l′ , if B holds for l′ , then it also holds for (x′ :: l′ );
—B L and Γ imply C.
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

Table III.

·

11

Definitional clauses for predicates over lists
△

length nil z = ⊤
△

length (X :: L) (s I) = length L I
△

list L = ∃i(nat i ∧ length L i)
△

element X (X :: L) = ⊤
△

element X (Y :: L) = element X L
△

split nil nil nil = ⊤
△

split (X :: L1 ) (X :: L2 ) L3 = split L1 L2 L3
△

split (X :: L1 ) L2 (X :: L3 ) = split L1 L2 L3
△

permute nil nil = ⊤
△

permute (X :: L1 ) L2 = ∃l22 (split L2 (X :: nil) l22 ∧ permute L1 l22 )

The proof is by induction on the length of the list L. Since list L holds, by
definition L has a length which is a natural number:
nat i, length L i, Γ −→ C
∧L
nat i, nat i ∧ length L i, Γ −→ C
∧L
nat i ∧ length L i, nat i ∧ length L i, Γ −→ C
cL
nat i ∧ length L i, Γ −→ C
∃L
∃i(nat i ∧ length L i), Γ −→ C
defL .
list L, Γ −→ C
We now claim that B holds for lists of any length, and wish to prove this claim
by induction on the length of the list. Thus we must prove
(1) the base case: B holds for lists of length zero;
(2) the induction step: if B holds for lists of length i′ , it holds for lists of length
(s i′ );
(3) the relevance of the claim: C follows from Γ, the fact that L has length i, and
the fact that B holds for lists of length i.
This is represented in F Oλ∆IN by applying the natL rule with the induction predicate λi.∀l(length l i ⊃ B l), which yields the three sequents
−→ ∀l(length l z ⊃ B l)
∀l(length l i′ ⊃ B l) −→ ∀l(length l (s i′ ) ⊃ B l)
∀l(length l i ⊃ B l), length L i, Γ −→ C .
Once we have proved that B holds for lists of length i, then we know it holds
for L. Thus we know that C follows from Γ, since our third working assumption
says that C follows from B L and Γ. This is represented formally by the partial
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

12

·

R. C. McDowell and D. A. Miller

derivation of the third premise of the natL rule:
init
length L i, Γ −→ length L i
B L, length L i, Γ −→ C
⊃L
length L i ⊃ B L, length L i, Γ −→ C
∀L .
∀l(length l i ⊃ B l), length L i, Γ −→ C
The unproved premise of this partial derivation is actually a weakening of the third
premise of the induction rule we are deriving. We do not have an explicit weakening
rule in F Oλ∆IN , but it suffices here to use the cut rule:
B L, length L i −→ B L B L, Γ −→ C
cut .
B L, length L i, Γ −→ C
The first premise of the cut rule is derivable for any B and L, since the consequent
B L also occurs as an antecedent. The second premise is the desired premise of the
rule we are deriving.
In the base case of the induction, we must show that B holds for lists of length
zero. Since the only list of length zero is nil, this follows from the first working
assumption, which says that B nil holds. This case is formalized in the following
partial derivation of the first premise of the natL rule:
⊤ −→ B nil
defL
length l z −→ B l
⊃R
−→ length l z ⊃ B l
∀R .
−→ ∀l(length l z ⊃ B l)
The induction step requires us to prove that B holds for all lists of length (s i′ ),
given that it holds for all lists of length i′ . Since a list of length (s i′ ) is constructed
by adding an element to the front of a list of length i′ , this step follows from the
second working assumption, which says that if B holds for a list l, then for any
x : τ , B holds for x :: l. This reasoning is represented in the partial derivation of
the second premise of the natL rule:
init
length l′ i′ −→ length l′ i′
B l′ , length l′ i′ −→ B (x′ :: l′ )
⊃L
′ ′
′
length l i ⊃ B l , length l′ i′ −→ B (x′ :: l′ )
∀L
∀l(length l i′ ⊃ B l), length l′ i′ −→ B (x′ :: l′ )
defL
∀l(length l i′ ⊃ B l), length l (s i′ ) −→ B l
⊃
R
∀l(length l i′ ⊃ B l) −→ length l (s i′ ) ⊃ B l
∀R .
∀l(length l i′ ⊃ B l) −→ ∀l(length l (s i′ ) ⊃ B l)
In this use of the defL rule, the complete set of unifiers for the atomic formula
△
length l (s i′ ) and the head of the clause ∀x′ , l′ , j[length (x′ :: l′ ) (s j) = length l′ j]
′
′
′
is the singleton set {[x :: l /l, i /j]}. The unproved premise of the partial derivation
above is a weakening of the second premise of the induction rule we are deriving.
We can achieve this weakening using the cut rule in the same manner as we did for
the third premise:
B l′ , length l′ i′ −→ B l′ B l′ −→ B (x′ :: l′ )
cut .
B l′ , length l′ i′ −→ B (x′ :: l′ )
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

·

13

We will now use this derived induction rule for lists to prove a very simple property, namely that we can split any list L into nil and L.
Proposition 2.6. The formula ∀l(list l ⊃ split l nil l) is derivable in F Oλ∆IN
using the definition D(list (τ )).
Proof. We prove this by induction on l; using the right rules for ∀ and ⊃ and
the derived rule of Proposition 2.5 with the induction predicate (λl.split l nil l), we
get the three sequents
−→ split nil nil nil
split l′ nil l′ −→ split (x′ :: l′ ) nil (x′ :: l′ )
split l nil l −→ split l nil l .
Since the induction predicate applied to l is the same as the consequent, the relevance of the induction predicate is immediate. Thus the third sequent follows from
the init rule.
The base case follows immediately from the definition of split, and so the first
sequent is derivable using the defR and ⊤R rules.
The induction step also follows easily from the definition of split:
init
split l′ nil l′ −→ split l′ nil l′
defR .
split l′ nil l′ −→ split (x′ :: l′ ) nil (x′ :: l′ )
We conclude this section with a proposition that presents additional properties
of lists that we have derived in F Oλ∆IN , though we omit the derivations here.
Proposition 2.7. The following formulas are derivable in F Oλ∆IN using the
definition D(list (τ )):
∀l(list l ⊃ ∀l1 ∀l2 (split l l1 l2 ⊃ (list l1 ∧ list l2 )))
∀l1 (list l1 ⊃ ∀l2 (list l2 ⊃ ∀l(split l l1 l2 ⊃ list l)))
∀l(list l ⊃ ∀l1 ∀l2 (split l l1 l2 ⊃ (∀x(element x l1 ⊃ element x l)∧
∀x(element x l2 ⊃ element x l))))
∀l(list l ⊃ ∀l1 ∀l2 (split l l1 l2 ⊃ split l l2 l1 ))
∀l(list l ⊃ ∀l23 ∀l1 ∀l2 ∀l3 (split l l1 l23 ⊃ split l23 l2 l3 ⊃ ∃l12 (split l l12 l3 ∧
split l12 l1 l2 )))
∀l(list l ⊃ ∀l12 ∀l1 ∀l2 ∀l3 (split l l12 l3 ⊃ split l12 l1 l2 ⊃ ∃l23 (split l l1 l23 ∧
split l23 l2 l3 )))
∀l(list l ⊃ permute l l )
∀l(list l ⊃ ∀l′ (permute l l′ ⊃ list l′ ))
∀l(list l ⊃ ∀l′ ∀l1 ∀l2 (list l′ ⊃ permute l l′ ⊃ split l l1 l2 ⊃
∃l1′ ∃l2′ (permute l1 l1′ ∧ permute l2 l2′ ∧ split l′ l1′ l2′ )))
∀l(list l ⊃ ∀l′ ∀l1 ∀l1′ ∀l2 ∀l2′ (list l′ ⊃ split l l1 l2 ⊃ split l′ l1′ l2′ ⊃
permute l1 l1′ ⊃ permute l2 l2′ ⊃ permute l l′ )) .
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

14

·

R. C. McDowell and D. A. Miller

3. THE STRENGTH OF F Oλ∆IN
Before proceeding to consider F Oλ∆IN as a logic for meta-theoretic analysis, we
comment here on how to relate F Oλ∆IN to other logical systems.
First, we show that F Oλ∆IN captures the theorems of an intuitionistic version
of Peano’s arithmetic (IPA) using a definition consisting of one clause for equality.
The formulas of IPA are those of a first-order logic with equality using the same
logical connectives as those in F Oλ∆IN and the same symbols z for zero and s for
successor. The axiom schemes for IPA can be grouped into the following collections.
(1) Axioms for first-order intuitionistic logic.
(2) Axioms for equality: reflexivity, symmetry, transitivity, and substitution.
(3) The two formulas
∀x∀y(s x = s y ⊃ x = y) and

∀x(z = s x ⊃⊥) .

(4) The axioms of induction: all formulas of the form
ϕ(z) ∧ ∀j(ϕ(j) ⊃ ϕ(s j)) ⊃ ∀xϕ(x) ,
where ϕ(x) ranges over formulas with at most the variable x free.
There are two inference rules for IPA: Modus Ponens allows the formula B to be
inferred from the formulas A ⊃ B and A, while Universal Generalization allows the
formula ∀xB to be inferred from B. A list of formulas C1 , . . . , Cn (n ≥ 1) is an
IPA derivation if for every i ∈ {1, . . . , n}, Ci is either an axiom or is the conclusion
of modus ponens or universal generalization from formulas in the list C1 , . . . , Ci−1 .
We write ⊢ipa C if C is the last formula of an IPA derivation.
In order to map an IPA formula, say B, to a F Oλ∆IN formula, say (B)◦ , we
must adjust for typing. The single sort used in IPA formulas will be mapped to
the type nt, and all instances of quantifiers in IPA formulas must be qualified
using the nat predicate: that is, (∀x.B)◦ = ∀x.nat x ⊃ (B)◦ and (∃x.B)◦ =
∃x.nat x ∧ (B)◦ . Predicates in IPA will be mapped to the corresponding predicates
in F Oλ∆IN similarly adjusted for type. Let D(eq) be the definition consisting of
the one clause:
△

I=I=⊤ .
We now sketch a proof that ⊢ipa C implies that (C)◦ has a F Oλ∆IN derivation
using D(eq). The proof is by induction on the length of IPA derivation. The axioms
of intuitionistic logic are derivable in F Oλ∆IN since it is complete for intuitionistic
logic (the rules for definition and natural numbers are not needed). The axioms
for equality are derivable using the definition rules with D(eq) (as noted in Girard
[1992] and Schroeder-Heister [1993]). The two formulas concerning z and s are also
derivable using the definition rules. The only remaining axiom that needs to be
considered is that for induction in IPA. Let φ(x) be a formula with at most x free
and let φ◦ (x) be the translation of that formula into F Oλ∆IN . We then need to
prove that the sequent
−→ φ◦ (z) ∧ ∀j(nat j ⊃ φ◦ (j) ⊃ φ◦ (s j)) ⊃ ∀x(nat x ⊃ φ◦ (x))
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

·

15

is derivable in F Oλ∆IN . Using the inference rules ⊃ R, ∀R, and cL, the derivability
of this sequent can be reduced to the derivability of the sequent
φ◦ (z) ∧ ∀j(nat j ⊃ φ◦ (j) ⊃ φ◦ (s j)), nat I, nat I −→ φ◦ (I) ,
where I is a new eigenvariable. Consider now deriving this sequent with natL,
using the induction predicate
λw. (φ◦ (z) ∧ ∀j(nat j ⊃ φ◦ (j) ⊃ φ◦ (s j)) ∧ nat w) ⊃ φ◦ (w) .
The three premises of this instance of natL are now easily derived.
Second, it may be possible to base the logic F Oλ∆IN on classical instead of
intuitionistic logic. Since F Oλ∆IN is intended to formalize informal mathematical
reasoning about computation, such a choice might well be interesting and useful,
although none of the many example applications we have explored require leaving
intuitionistic logic. We do not explore a classical version of F Oλ∆IN here and simply
point out that if the classical variant satisfies a cut-elimination property, a proof of
that fact does not seem to be a straightforward generalization of the proof given in
McDowell [1997] and McDowell and Miller [2000].
Finally, we add a word about how F Oλ∆IN can be used to reason about computation. Subsets of intuitionistic logic, such as herditary Harrop formulas or Horn
clauses can be used to specify computation using goal-directed derivation search
[Miller et al. 1991]. The logic F Oλ∆IN , which is much stronger than these subsets,
can be used to reason about logic programs in the following fashion. Let P be,
for example, a Horn clause program and let G be some goal formula (a formula
composed of conjunctions, disjunctions, and existential quantifiers) such that there
is goal-directed derivation of the sequent P −→ G in intuitionistic logic. That
derivation is also a cut-free intuitionistic logic derivation [Miller et al. 1991]. Thus
the sequent −→ G has a cut-free derivation in F Oλ∆IN using P as a definition
(given the restrictions on G and P, there are no occurrences of the defL and natL
inference rules in such a derivation). Now assume that we have also a derivation in
F Oλ∆IN using P as a definition of the sequent G −→ G′ , for some goal formula G′ .
Using the cut-elimination theorem for F Oλ∆IN (Proposition 1.1), we know that the
sequent −→ G′ has a cut-free derivation in F Oλ∆IN using P as a definition. Since
induction is encoded as a left-introduction rule, it is easy to see that the resulting
derivation does not contain occurrences of induction. Similarly, there can be no
occurrences of the defL rule. Hence, we can conclude that P −→ G′ will have an
intuitionistic logic derivation as well as a goal-directed derivation. Thus, informally,
we can conclude that if G ⊃ G′ is derivable in F Oλ∆IN and there is a computation proving G, then there is computation proving G′ . Hence, implications in the
stronger logic can be used to show that the existence of certain computations can
lead to the existence of other computations. For example, as we have mentioned in
Proposition 2.7, the formula
∀l(list l ⊃ ∀l1 ∀l2 (split l l1 l2 ⊃ split l l2 l1 ))
can be derived in F Oλ∆IN using D(list (τ )). If we also assume that we are given
three lists L0 , L1 , L2 such that list L0 and split L0 L1 L2 follow from D(list (τ ))
(considered as a Horn clause logic program), then the above argument can be used
to show that split L0 L2 L1 must also follow from that logic program.
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

16

·

R. C. McDowell and D. A. Miller

Part II: LOGIC REPRESENTATIONS FOR META-THEORETIC ANALYSIS
Since F Oλ∆IN contains quantification at higher-order types and term structures
involving λ-terms, it easily supports higher-order abstract syntax. Eriksson [1993]
demonstrated the use of his finitary calculus of partial inductive definitions (which
is similar to F Oλ∆IN ) for the specification of various logics and type systems using higher-order abstract syntax. Our goal is to go a step beyond that and also
reason within F Oλ∆IN about the object systems. As we set about to do so, we
encounter some difficulties in reasoning about higher-order abstract syntax specifications within the specification logic and develop strategies for surmounting those
difficulties.
We begin the first section of this part by presenting the usual higher-order abstract syntax representation of intuitionistic logic and illustrating the problems
alluded to above. We then proceed through several modifications of this encoding
which improve our ability to perform meta-theoretic analyses, although at some loss
of the benefits of higher-order abstract syntax. In Section 5 we further illustrate
these encoding techniques through two examples involving fragments of intuitionistic and linear logic. The specifications of these two logics will also be used in Part
III as part of an alternative strategy for formal reasoning with higher-order abstract
syntax that retains the full benefits of this representation style. We conclude the
present part with a section discussing related work.
To keep our discussion succinct, we do not prove the adequacy of the encodings
presented in Section 4. The skeptical reader is referred to the discussion of similar
encodings in the literature: see Section 6 for references. The two encodings of
Section 5, however, play a key role in our work, and so we do include adequacy
theorems for these.
4. A SPECTRUM OF ENCODING STYLES
4.1 Natural deduction-style encoding
In order to examine our ability to reason about higher-order abstract syntax encodings in F Oλ∆IN , we present a definition of first-order intuitionistic logic. For
brevity we will restrict our discussion here to a fragment of the logic containing implication and quantification. The full logic is considered in McDowell [1997], though
the remaining connectives do not provide any additional insight. We use the type i
for terms of the object logic, the type atm for atoms (atomic propositions) and the
type prp for general propositions; we also introduce the following constants:
V
h i : atm → prp
Wi : (i → prp) → prp
⇒ : prp → prp → prp
i : (i → prp) → prp .
The constant h i coerces atoms into propositions: object-level predicates will be constants that build meta-level
V termsWof type atm. The constant ⇒ represents the implication connective and i and i encode universal and existential quantification
at type i. Notice that we are using the λ-abstraction of F Oλ∆IN ’s term language
to represent the variable binding of the two object logic quantifiers. As a result,
α-equivalence of quantified object logic formulas follows from the α-equivalence
of λ-bound terms in F Oλ∆IN , and substitution for object logic variables can be
accomplished by β-reduction at the level of F Oλ∆IN terms.
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

Table IV.

·

17

Natural deduction encoding of intuitionistic logic

prove (B ⇒
V C) ⊂ prove B ⊃ prove C
prove Wi B ⊂ ∀i x prove (B x)
B ⊂ ∃i x prove (B x)
prove
i
prove C ⊂ ∃b(prove
V (b ⇒ C) ∧ prove b)
B
prove (B X) ⊂ prove
iW
b ∧ (∃i x prove (b x) ⊃ prove C))
prove C ⊂ ∃b(prove
i

Derivability in the object logic is encoded via the predicate prove of type prp → o;
the usual higher-order abstract syntax encoding of this predicate is the theory shown
in Table IV. Here we use ⊂ for reverse implication in the meta-logic; the first clause,
for example, can be rewritten as
(prove B ⊃ prove C) ⊃ prove (B ⇒ C) .
The first three clauses correspond to the introduction rules for natural deduction;
the remaining three correspond to the elimination rules.
Although this encoding mirrors the rules for natural deduction, we may view
it as an encoding of the sequent calculus, with the derivability of the sequent
B1 , . . . , Bn −→ C represented by the F Oλ∆IN formula
prove B1 ⊃ · · · ⊃ prove Bn ⊃ prove C .
This is in keeping with the higher-order abstract syntax principle of using specification logic hypotheses to represent contexts (in this case, the left side of the
sequent). The structural rules (exchange, weakening, and contraction) follow immediately from this representation; for example, the derivation for weakening is
init
⊃R
−→ prove c ⊃ (prove b ⊃ prove c)
∀R .
−→ ∀b∀c(prove c ⊃ (prove b ⊃ prove c))
prove c, prove b −→ prove c

We use double horizontal lines to represent multiple applications of an inference
rule. In this case, both the ⊃ R rule and the ∀R rule are applied twice. The
admissibility of the cut rule, encoded by the formula
∀b∀c((prove b ⊃ prove c) ⊃ prove b ⊃ prove c) ,
also follows easily from the ⊃ L rule. The right rules are the same as the corresponding introduction rules, and the left rules are easilyVderived from the clauses for
the corresponding elimination rules. The left rule for i , for instance, is encoded
by the F Oλ∆IN formula
V
∀b∀c(∃x(prove (b x) ⊃ prove c) ⊃ (prove i b ⊃ prove c)) ,
V
whose derivation is evident from the clause for the elimination rule for i .
However, this encoding is not appropriate for meta-theoretic analysis of object
logic derivations. To do such analysis in F Oλ∆IN , we need to be able to perform
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

18

·

R. C. McDowell and D. A. Miller

Table V.

Sequent calculus encoding of intuitionistic logic
△

concI hAi = hyp hAi
△

conc(s I) (B ⇒ C) = hyp B ⊃ concI C
conc(s I)
conc(s I)

V
B
Wi
i

△

= ∀i x concI (B x)
△

B = ∃i x concI (B x)
△

conc(s I) D = ∃b∃c(hyp (b ⇒ c) ∧ (hyp c ⊃ concI D) ∧ concI b)
△

conc(s I) C = ∃b(hyp
△

conc(s I) C = ∃b(hyp

V
b
Wi

∧ (∀i x hyp (b x) ⊃ concI C))

b ∧ (∃i x hyp (b x) ⊃ concI C))
i

induction over the derivations. Recall that in Section 2.2 we used the natural
number measure in the length predicate to derive an induction principle for lists.
But there is no apparent way to add a natural number induction measure to the
prove predicate because of the clause for the ⇒ introduction rule. This reflects the
fact that this clause gives rise to a non-monotone operator; this is generally true
of the types and theories in higher-order abstract syntax encodings, and makes
inductive principles difficult to find. We would also like to change the specification
into a definition so that we can use the defL rule for the analysis of derivations.
△
Simply replacing the ⊂ in each clause by = is problematic for two reasons. First,
the clause resulting from the introduction rule for ⇒ would not satisfy the level
restriction for any level we
V might assign to prove. Second, the clause resulting from
the elimination rule for i would have a problematic head. There are too many
ways that (B X) can match and unify with other terms; this makes the practical
application of the defR and defL rules difficult and would result in many cases that
are not productive.
4.2 Sequent calculus-style encoding
We can solve the problems with the encoding of the introduction rule for ⇒ by
introducing separate predicates
hyp : prp → o

conc : nt → prp → o

for the left and right sides of the sequent, respectively. The predicate hyp will not
be a defined predicate, and so can have level zero. The negative occurrence of prove
in the introduction clause for ⇒ becomes an occurence of hyp, so the predicate conc
can then have level one. This also makes possible the assignment of a measure to
conc, as suggested by its type. To emphasize that the first argument to conc is a
measure, we
V will write it as a subscript. The problem introduced by the elimination
clause for i is avoided by patterning the encoding after the sequent calculus rules
rather than natural deduction rules. The resulting definition is shown in Table V.
The first clause encodes the initial axiom, the next three correspond to the right
introduction rules, and the remaining three correspond to the left introduction
rules.
Since we have not changed the representation of quantification, we get α-equivalence of quantified object logic formulas and substitution for object logic variables
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

·

19

from the relevant features of F Oλ∆IN as before. We are still using F Oλ∆IN hypotheses to represent contexts, so the structural rules also follow as before. However, the
admissibility of the cut rule, now encoded as
∀b∀c(∃i(hyp b ⊃ conci c) ⊃ ∃i conci b ⊃ ∃i conci c) ,
is no longer immediate: there is no simple proof of ∃i conci b −→ hyp b. We
expect, though, that the admissibility of cut is still derivable in F Oλ∆IN following
the method of Pfenning [1995].
This encoding has another limitation; to see it, consider the following example.
Suppose we know that the sequent b ⇒ a −→ a is derivable in intuitionistic logic
for some atom a and proposition b. Since a is atomic, the derivation must end
with a left rule, and since the only formula on the left is b ⇒ a, it must be the left
implication rule. Thus there are derivations of b ⇒ a −→ b and a, b ⇒ a −→ a.
This second sequent is not so interesting, since it is an initial sequent. So we have
shown that if b ⇒ a −→ a is derivable then b ⇒ a −→ b is as well.
Now let us try to capture this reasoning in F Oλ∆IN using our current encoding
of intuitionistic logic. We want to derive the sequent
−→ ∀a∀b(∃i(hyp (b ⇒ hai) ⊃ conci hai) ⊃ ∃j(hyp (b ⇒ hai) ⊃ concj b)) .
After the obvious uses of ∀R and ⊃ R, we get
∃i(hyp (b ⇒ hai) ⊃ conci hai) −→ ∃j(hyp (b ⇒ hai) ⊃ concj b) .
From our informal reasoning, we know that the derivation of b will have a smaller
measure than the derivation of a; thus in applying the ∃L and ∃R rules it is
conservative to substitute i for j:
hyp (b ⇒ hai) ⊃ conci hai −→ hyp (b ⇒ hai) ⊃ conci b .
To follow the informal proof, we now want to indicate that hyp (b ⇒ hai) ⊃
conci hai must be true by the definitional clause encoding the left ⇒ rule. However,
we cannot apply the defL rule to this formula, since it is not an atom. The closest
thing to this that we can do is to eliminate the ⊃ and then apply defL to conci hai.
We can eliminate the ⊃ by using ⊃ R and then ⊃ L, yielding the two sequents
hyp (b ⇒ hai) −→ hyp (b ⇒ hai)
conci hai, hyp (b ⇒ hai) −→ conci b .
The first is immediate by the init rule. Applying the defL rule to conci hai in the
second sequent yields four sequents corresponding to the cases where the derivation
of a ends with the initial rule or any of the three left rules:
hyp hai, hyp (b ⇒ hai) −→ conci b
∃b′ ∃c′ (hyp (b′ ⇒ c′ ) ∧ (hyp c′ ⊃ conci′ hai) ∧ conci′ b′ ), hyp (b ⇒ hai) −→
conc(s i′ ) b
V
∃b′ (hyp i b′ ∧ (∀i x hyp (b′ x) ⊃ conci′ hai)), hyp (b ⇒ hai) −→ conc(s i′ ) b
∃b′ (hyp

W

i

b′ ∧ (∃i x hyp (b′ x) ⊃ conci′ hai)), hyp (b ⇒ hai) −→ conc(s i′ ) b .
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

20

·

R. C. McDowell and D. A. Miller

Table VI.

Explicit sequent encoding of intuitionistic logic
△

seqI L hAi = element hAi L
△

seq(s I) L (B ⇒ C) = seqI (B :: L) C

V
seq(s I) L ( i B)
W
seq(s I) L (

i

△

= ∀i x seqI L (B x)
△

B) = ∃i x seqI L (B x)
△

seq(s I) L D = ∃b∃c(element (b ⇒ c) L ∧ seqI (c :: L) D ∧ seqI L b)
△

seq(s I) L C = ∃b(element
△

seq(s I) L C = ∃b(element

V
bL
Wi
i

∧ ∃i x seqI ((b x) :: L) C)

b L ∧ ∀i x seqI ((b x) :: L) C)

This is clearly not what we want. Even in the case corresponding to the left ⇒ rule
we do not know that the rule was applied to the implication b ⇒ hai. There are
really two problems here. The first is that hyp (b ⇒ hai) ⊃ conci hai expresses the
idea that b ⇒ hai is a hypothesis available in the derivation of conci hai, but it does
not capture the idea that it is the only hypothesis available. Thus the defL rule
forces us to consider derivations ending with the initial rule or any of the left rules,
since the appropriate formula may be available as a hypothesis. The second problem
is that we do not have any way to examine the different ways of deriving something
from a specific set of hypotheses. Although the formula hyp (b ⇒ hai) ⊃ conci hai
indicates that the atom a is derivable from the hypothesis b ⇒ hai, we cannot
examine how that derivation might take place. All we can do is use the ⊃ L rule,
which says that we know that the hypothesis b ⇒ hai is available and so can
conclude that a holds.
4.3 Explicit sequent encoding
To remedy this situation, we explicitly represent the entire sequent in a single
atomic judgement. As a result, the relevant object logic hypotheses are known
to be exactly those listed in the judgement, and the defL rule can be applied to
the judgement to examine how the corresponding sequent might be derived. Thus
derivability is encoded via the predicate
seq : nt → prplst → prp → o .
The first argument is an induction measure and will be displayed as a subscript.
The second argument is a list of terms of type prp and represents the left side of
the sequent. We will assume that prplst is the same as the type lst introduced in
Section 2.2, using prp for the type of elements. In particular we will assume that we
have constructors nil and ::, and a predicate element as defined in D(list (prp)). The
third argument to seq corresponds to the right side of the sequent. The definition
for this predicate is shown in Table VI.
Since we have not changed the representation of quantification, we get α-equivalence of quantified object logic formulas and substitution for object logic variables
from the relevant features of F Oλ∆IN as before. We are no longer using F Oλ∆IN
hypotheses to represent contexts, however, so the structural rules must now be
derived by induction. The admissibility of the cut rule must also be derived by
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

·

21

induction, as was the case with the previous encoding. With the atomic encoding
of sequents, we now can analyze derivations of propositions from hypotheses. To
see this, we revisit the example from above. To formalize this example with the
encoding of Table VI, we derive the sequent
−→ ∀a∀b(∃i seqi ((b ⇒ hai) :: nil) hai ⊃ ∃j seqj ((b ⇒ hai) :: nil) b) .
Applying the ∀R, ⊃ R, and ∃L rules yields the sequent
seqi ((b ⇒ hai) :: nil) hai −→ ∃j seqj ((b ⇒ hai) :: nil) b .
Now we apply the defL rule to the judgement on the left, which yields four sequents,
again corresponding to the cases where the derivation of a ends with the initial rule
or any of the three left rules:
element hai ((b ⇒ hai) :: nil) −→ ∃j seqj ((b ⇒ hai) :: nil) b
∃b′ ∃c′ (element (b′ ⇒ c′ ) ((b ⇒ hai) :: nil) ∧
seqi′ (c′ :: (b ⇒ hai) :: nil) hai ∧
seqi′ ((b ⇒ hai) :: nil) b′ ) −→ ∃j seqj ((b ⇒ hai) :: nil) b
V
∃b′ (element i b′ ((b ⇒ hai) :: nil) ∧
∃i x seqi′ ((b′ x) :: (b ⇒ hai) :: nil) hai) −→ ∃j seqj ((b ⇒ hai) :: nil) b
W
∃b′ (element i b′ ((b ⇒ hai) :: nil) ∧
∀i x seqi′ ((b′ x) :: (b ⇒ hai) :: nil) hai) −→ ∃j seqj ((b ⇒ hai) :: nil) b .
But this time we can easily eliminate three of the four possibilities, since the element assumption is obviously false. In the first sequent, for example, we have the
assumption element hai ((b ⇒ hai) :: nil). Since hai cannot unify with (b ⇒ hai),
hai cannot be the first element of the list; therefore it must be an element of the
remainder. But the remainder is the empty list, so hai cannot be an element of it
either. This is accomplished formally by applying the defL rule twice:
element hai nil −→ ∃j seqj ((b ⇒ hai) :: nil) b

defL

element hai ((b ⇒ hai) :: nil) −→ ∃j seqj ((b ⇒ hai) :: nil) b

defL .

The remaining cases are done similarly, except for the one valid case, which corresponds to a use of the left ⇒ rule:
∃b′ ∃c′ (element (b′ ⇒ c′ ) ((b ⇒ hai) :: nil) ∧
seqi′ (c′ :: (b ⇒ hai) :: nil) hai ∧
seqi′ ((b ⇒ hai) :: nil) b′ ) −→ ∃j seqj ((b ⇒ hai) :: nil) b .
In this case, b′ ⇒ c′ does match the first element of the list, so we must consider
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

22

·

R. C. McDowell and D. A. Miller

the case where the left ⇒ rule was applied to (b ⇒ hai):
defL
⊤, seqi′ ((b ⇒ hai) :: nil) b −→ ∃j . . . element (b′ ⇒ c′ ) nil, . . . −→ ∃j . . .
defL
element (b′ ⇒ c′ ) ((b ⇒ hai) :: nil), seqi′ ((b ⇒ hai) :: nil) b′ −→ ∃j . . .
∧L
element (b′ ⇒ c′ ) . . . ∧ . . . , element (b′ ⇒ c′ ) . . . ∧ . . . −→ ∃j . . .
cL
element (b′ ⇒ c′ ) ((b ⇒ hai) :: nil) ∧ . . . −→ ∃j seqj ((b ⇒ hai) :: nil) b
∃L .
. . . −→ ∃j seqj ((b ⇒ hai) :: nil) b
But the unproved sequent is easily derived by choosing j to be i′ :
init
⊤, seqi′ ((b ⇒ hai) :: nil) b −→ seqi′ ((b ⇒ hai) :: nil) b
∃R .
⊤, seqi′ ((b ⇒ hai) :: nil) b −→ ∃j seqj ((b ⇒ hai) :: nil) b
Now let us consider another example. Suppose we know that the sequent
^ ^
−→
y1 y2 (p y1 t1 ⇒ p y2 t2 ⇒ p y2 t3 )
is derivable in intuitionistic logic for some predicate constant p and some terms
V
t1 , t2 , and t3 . The derivation must end with applications of the right rules for
and ⇒, since these are the only rules that apply. Thus we know that the sequent
p y1 t1 , p y2 t2 −→ p y2 t3 is derivable. Since p is a predicate constant, these formulas
are all atomic, so the only rule that applies is the
V initial rule. The eigenvariable
condition for the application of the right rule for
guarantees that y1 and y2 are
distinct, so the initial rule must apply to the second hypothesis. Therefore, it must
be the case that t2 and t3 are the same term.
Now let us try to capture this reasoning in F Oλ∆IN using our current encoding
of intuitionistic logic. To do this, we will need some way to indicate term identity,
and so we introduce the predicate ≡ of type i → i → o defined by the clause
△
X ≡ X = ⊤. We then want to derive the sequent
V
V
−→∀p∀t1 ∀t2 ∀t3 (∃i seqi nil i y1 i y2 (hp y1 t1 i ⇒ hp y2 t2 i ⇒ hp y2 t3 i) ⊃ t2 ≡ t3 ).
The only way to proceed is by applying ∀R and ⊃ R, yielding
V
V
∃i seqi nil i y1 i y2 (hp y1 t1 i ⇒ hp y2 t2 i ⇒ hp y2 t3 i) −→ t2 ≡ t3 .
There is nothing more that we can do on the right, since the definitional clause for
≡ does not apply. Applying ∃L gives us the sequent
V
V
seqi nil i y1 i y2 (hp y1 t1 i ⇒ hp y2 t2 i ⇒ hp y2 t3 i) −→ t2 ≡ t3 .
V
V
Now we want to reason about the derivation of i y1 i y2 . . . to conclude that
t2 ≡ t3 . In theVinformal proof, we reasoned that this derivation must end with the
right rule for ; we do the same thing here using defL, which yields the sequent
V
∀y1 seqi1 nil i y2 (hp y1 t1 i ⇒ hp y2 t2 i ⇒ hp y2 t3 i) −→ t2 ≡ t3 ,
as well as three other sequents corresponding to the cases where the object logic
derivation ends with the application of one of the left rules. Since these latter three
sequents represent cases that are not applicable, they are easily derivable as shown
in the previous example; we thus focus on the sequent shown above. Before we can
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

·

23

V
proceed to apply defL again for the second use of the right rule for , we must
first apply ∀L, which requires supplying a substitution term for y1 . For this proof,
it doesn’t matter what term we use for y1 , as long as it is something that does not
unify with the term we supply for y2 . So let x1 and x2 be two distinct, non-unifiable
terms of type i. If we use x1 for y1 , and then apply defL and ∀L again using x2 for
y2 , we get
seqi2 nil (hp x1 t1 i ⇒ hp x2 t2 i ⇒ hp x2 t3 i) −→ t2 ≡ t3 .
We now apply defL two more times, each of which corresponds to reasoning that
the object logic derivation must proceed with a use of the right rule for ⇒. This
yields the sequent
seqi3 (hp x2 t2 i :: hp x1 t1 i :: nil) hp x2 t3 i −→ t2 ≡ t3 .
Another application of defL reflects the fact that in the object logic derivation only
the initial rule now applies:
element hp x2 t3 i (hp x2 t2 i :: hp x1 t1 i :: nil) −→ t2 ≡ t3 .
For hp x2 t3 i to be the first element of the list, t2 and t3 must be the same, and this
is what we want to prove. We have chosen x1 and x2 to be terms that do not unify,
so hp x2 t3 i cannot be the other element of the list. This reasoning is represented
formally by the F Oλ∆IN derivation
defL
⊤R
element hp x2 t3 i nil −→ t2 ≡ t3
⊤ −→ ⊤
defL
defR
⊤ −→ t2 ≡ t2
element hp x2 t3 i (hp x1 t1 i :: nil) −→ t2 ≡ t3
defL .
element hp x2 t3 i (hp x2 t2 i :: hp x1 t1 i :: nil) −→ t2 ≡ t3
If we are able to construct the two non-unifiable terms x1 and x2 , we are able
to conduct this analysis in F Oλ∆IN . But the need for these two terms is rather
disturbing. The informal proof is independent of the type of y1 and y2 and the
term structure of this type. In fact, the informal proof is valid even for a type that
is uninhabited; this is obviously not the case for our representation in F Oλ∆IN .
The problem is that our representation of object-level quantification in terms of
F Oλ∆IN quantification doesn’t allow us to examine a derivation that is generic over
certain terms. Although the formula ∀y seqi L (B y) indicates that the proposition
B y is derivable from the hypotheses in L for any y, it does not indicate that the
derivation is the same for all y, and we cannot examine that derivation generically.
All we can do is use the ∀L rule, which requires us to substitute a specific term for
y, and then examine the derivation for that specific term. This is analagous to the
problem we encountered before related to the encoding of object logic implication
in terms of F Oλ∆IN implication.
4.4 Explicit eigenvariable encoding
To solve this problem we must explicitly keep track of the eigenvariables introduced
by the quantifier rules. We do not wish to abandon, however, our higher-order
abstract syntax representation of quantification. In the earlier encodings of this
section, we encoded the rules for object logic quantification using F Oλ∆IN quantification; the key idea of our solution is to replace that use of F Oλ∆IN quantification
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

24

·

R. C. McDowell and D. A. Miller

with the use of F Oλ∆IN λ-abstraction. If we follow this idea naively and simply
replace the quantification
by λ-abstraction, we get the following encoding of the
V
right rule for :
V
△
seq(s I) L ( i B) = λx seqI L (B x) .
This does not work, of course, since the body of this clause now has type i → o
instead of type o. To address this problem, it is important to first realize that as
more eigenvariables are added and propositions are moved between the left and
right sides of the sequent, we must deal more generally with “judgements” of the
form
λx1 . . . λxn seqI (L x1 . . . xn ) (B x1 . . . xn )
for arbitrary n ≥ 0. First consider “uncurrying” this expression by replacing the λabstractions over x1 , . . . , xn by a single λ-abstraction over the n-tuple (x1 , . . . , xn ):
λx.seqI (L (π1 x) . . . (πn x)) (B (π1 x) . . . (πn x)) .
Now we can deal with the arbitrary n by replacing the n-tuple with a list, and using
fst x in place of π1 x, fst (rst x) in place of π2 x, fst (rst (rst x)) in place of π3 x,
etc. Finally, we push the λ-abstraction into the seq predicate by changing its type:
seq : nt → (evs → prplst) → (evs → prp) → o .
Here evs is a new type representing a list of eigenvariables. We have already seen
the two operators on this type, fst: evs → i and rst: evs → evs; fst l represents the
first eigenvariable
V in the list l, and rst l represents the remainder of the list. The
right rule for
is now encoded as follows:
V
△
seq(s I) L (λl i x(B l x)) = seqI (λl′ L(rst l′ )) (λl′ B (rst l′ ) (fst l′ )) .
The bound variable l′ in the body of the clause should be thought of as a list whose
length is one longer than the length of the bound variable l in the head of the clause;
′
fst l′ represents the
W new eigenvariable, and rst l represents the eigenvariables in l.
The left rule for i is similarly modified:
W
△
seq(s I) L C = ∃b(element (λl i x(b l x)) L ∧
seqI (λl′ (b (rst l′ ) (fst l′ )) :: (L (rst l′ ))) (λl′ C (rst l′ )) .
The remainder of the clauses are only modified to reflect the change in the type
∆IN
of seq. Note in particular that
quantification
V F Oλ
W can still be used in the
encodings of the left rule for
and the right rule for ; since these rules do not
introduce eigenvariables, this use of F Oλ∆IN quantification is not problematic. The
type of the predicate element also changes:
element : (evs → prp) → (evs → prplst) → o .
Table VII presents the definition for the entire logic.
Since we have not changed the representation of quantification, we get α-equivalence of quantified object logic formulas and substitution for object logic bound
variables from the relevant features of F Oλ∆IN as before. Substitution for eigenvariables is a little more involved, as shown by its encoding via the predicates
subst : nt → (evs → i) → (evs → i) → (evs → i) → o
subst0 : nt → (evs → evs → i) → (evs → evs → i) → (evs → evs → i) → o .
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

Table VII.

·

25

Explicit eigenvariable encoding of intuitionistic logic
△

seqI L λl h(A l)i = element λl h(A l)i L
△

seq(s I) L λl ((B l) ⇒ (C l)) = seqI λl ((B l) :: (L l)) C

V
seq(s I) L (λl i x(B l x))
W

seq(s I) L (λl

i

△

= seqI (λl′ L (rst l′ )) (λl′ B (rst l′ ) (fst l′ ))
△

x(B l x)) = ∃x seqI L (λl B l (x l))
△

seq(s I) L D = ∃b∃c(element λl ((b l) ⇒ (c l)) L ∧
seqI λl ((c l) :: (L l)) D ∧
seqI L b)
△

V

△

W

seq(s I) L C = ∃b(element (λl i x(b l x)) L ∧
∃x seqI λl ((b l (x l)) :: (L l)) C)
seq(s I) L C = ∃b(element (λl i x(b l x)) L ∧
seqI λl′ ((b (rst l′ ) (fst l′ )) :: (L (rst l′ ))) (λl′ C (rst l′ )))
△

element X λl ((X l) :: (L l)) = ⊤
△

element X λl ((Y l) :: (L l)) = element X L

Table VIII.

Encoding of substitution for eigenvariables

△

subst I T1 T2 T2′ = subst0 I (λl′ T1 ) (λl′ T2 ) (λl′ T2′ )
subst0 z T1 (λl′ λl T2 l′ (fst l) (rst l)) (λl′ λl T2 l′ (T1 l′ l) (rst l))
△

= ⊤
subst0 (s I) (λl′ λl T1 l′ (fst l) (rst l))
(λl′ λl T2 l′ (fst l) (rst l)) (λl′ λl T2′ l′ (fst l) (rst l))
△
= subst0 I (λl′ λl T1 (rst l′ ) (fst l′ ) l)
(λl′ λl T2 (rst l′ ) (fst l′ ) l) (λl′ λl T2′

(rst l′ ) (fst l′ ) l)

The judgement subst i t1 t2 t′2 indicates that t′2 is the result of substituting t1 in
t2 for the (i + 1)th eigenvariable. We could just as easily use the actual encoding
(fst (rsti l)) of the (i + 1)th eigenvariable in place of its index, but we find it more
convenient to use the index so that we can perform induction on it. (Here we use
(rsti l) for n applications of rst to l, i.e., (rst0 l) is l, (rst1 l) is (rst l), (rst2 l) is
(rst (rst l)), etc.) The subst0 predicate is used in the definition of subst; the extra
evs argument is used to keep track of eigenvariables at the beginning of the list as we
search down the list for the substitution variable. The encoding of these predicates
is shown in Table VIII. Substitution for the first eigenvariable can be done directly;
to substitute for the (i + 2)th eigenvariable we move the first eigenvariable from the
list l to the list l′ and substitute for the (i + 1)th eigenvariable of l.
As with the previous encoding of intuitionistic logic, we must derive the admissibility of the structural rules and the cut rule by induction. We have retained the
atomic encoding of sequents, so we can still analyze derivations of propositions from
hypotheses. In addition, the explicit encoding of eigenvariables allows us to better
analyze derivations of generic propositions. To see this, we revisit the example from
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

26

·

R. C. McDowell and D. A. Miller

before; the sequent we wish to derive is
V
V
−→ ∀p∀t1 ∀t2 ∀t3 (∃i seqi λl nil (λl i y1 i y2 (hp y1 t1 i ⇒ hp y2 t2 i ⇒ hp y2 t3 i)) ⊃
t2 ≡ t3 ) .
As before, we begin by applying the ∀R, ⊃ R, and ∃L rules to obtain the sequent
V
V
seqi λl nil (λl i y1 i y2 (hp y1 t1 i ⇒ hp y2 t2 i ⇒ hp y2 t3 i)) −→ t2 ≡ t3 .
V V
The derivation of the object
V logic formula y1 y2 . . . must end with two applications of the right rule for ; we formalize this by applying defL twice, which results
in the sequent
seqi1 λl nil λl (hp (fst (rst l)) t1 i ⇒ hp (fst l) t2 i ⇒ hp (fst l) t3 i) −→ t2 ≡ t3 .
The object logic derivation must proceed with two applications of the right rule for
⇒; we deduce this formally by two more applications of the defL rule, yielding
seqi2 λl (hp (fst l) t2 i :: hp (fst (rst l)) t1 i :: nil) λl hp (fst l) t3 i −→ t2 ≡ t3 .
An additional use of the defL rule corresponds to the realization that the initial
rule must complete the object logic derivation, giving us the sequent
element λl hp (fst l) t3 i λl (hp (fst l) t2 i :: hp (fst (rst l)) t1 i :: nil) −→ t2 ≡ t3 .
If hp (fst l) t3 i is the first element of the list, then t2 and t3 are the same, which is
the result we are trying to establish. The formula hp (fst l) t3 i cannot be the other
element of the list, because the first argument to p differs; thus we are done. This
is all formally encoded by the derivation
⊤R
element λl hp (fst l) t3 i (λl nil) −→ t2 ≡ t3
⊤ −→ ⊤
defR
⊤ −→ t2 ≡ t2
element λl hp (fst l) t3 i λl (hp (fst (rst l)) t1 i :: nil) −→ t2 ≡ t3
element λl hp (fst l) t3 i λl (hp (fst l) t2 i :: hp (fst (rst l)) t1 i :: nil) −→ t2 ≡ t3 ,
where the three inference rules without labels are defL.
4.5 Discussion
Before going on to formally derive theorems about encodings of logics, let us reflect
on the encoding styles we have discussed. What we have is a spectrum of styles,
all of which share the same higher-order abstract syntax encoding of formulas, but
which vary in the degree to which they use the higher-order abstract syntax encoding of inference rules. The first encoding used the typical higher-order abstract
syntax techniques, which made a number of significant properties of the object logic
fall out easily from the properties of F Oλ∆IN . Unfortunately this encoding did not
lend itself to formal analysis within F Oλ∆IN , since it could not be expressed as
a definition nor given an induction measure. We then progressed through three
other encodings, each of which compromised the use of higher-order abstract syntax a bit more. The cost of each compromise was a decrease in the elegance and
an increase in the complexity of the encoding, and a reduction in the extent to
which fundamental properties of the object logic followed from corresponding properties of F Oλ∆IN . The benefit, of course, was a greater ability to perform formal
meta-theoretic analysis.
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

·

27

In Part III we will discuss an approach which lets us use the typical higherorder abstract syntax encodings and also perform meta-theoretic analyses on these
encodings. The key to this approach is the use of a specification logic that is
separate from F Oλ∆IN , and in fact is itself specified in F Oλ∆IN . In the next section
we present two logics which will be used for this purpose, and which also serve as
examples of the last two encoding techniques discussed in this section.
5. REPRESENTATION AND ANALYSIS OF LOGICS
In this section we illustrate the use of the some of the encoding techniques just
presented. In Section 5.1 we use the explicit sequent technique of Section 4.3 to
encode a fragment of intuitionistic logic; Section 5.2 discusses a fragment of linear
logic encoded with the explicit eigenvariable technique of Section 4.4. In each case
we prove the adequacy of the encoding and also derive in F Oλ∆IN some properties
of the object logic.
5.1 Intuitionistic logic
Consider the fragment of second-order intuitionistic logic given by the grammar
V
V
D ::= A | G ⇒ A |
α→α
α x.D |
V x.D
G ::= A | tt | G & G | A ⇒ G |
α x.G ,
where A ranges over atomic formulas and α ranges over ground types. D and
G represent definite clauses and goal formulas, respectively. Although this seems
like a rather simple fragment, higher-order abstract syntax encodings generally fall
within the set of definite clauses given by this grammar. Full intuitionistic logic
could be used here instead, but its encoding is larger and that increase does not
contribute to the set of examples that we wish to use here. The set of goal formulas
can be encoded using the following constants:
V
h i : atm → prp
& : prp → prp → prp
i : (i → prp) → prp
tt : prp
⇒ : atm → prp → prp .
Notice that the antecendent of the implication is restricted to be atomic.
If we take any sequent calculus inference rule and restrict the conclusion to be a
sequent whose antecedents are definite clauses and whose consequent is a goal formula, then the premises will also be sequents of this form. In fact, any antecedent
in the premises will either be an antecedent of the conclusion or an atomic formula.
Thus in a derivation in this fragment of intuitionistic logic, all non-atomic antecedents in any sequent of the derivation appear as antecedents in the end-sequent.
So we can divide the antecedents into the original theory, which remains constant
throughout the derivation, and some atomic antecedents, which vary throughout
the derivation. Leaving the fixed theory aside for the moment, we can restrict our
sequents to have only atomic antecedents:
seq : nt → atmlst → prp → o ,
where atmlst is the same as the type lst introduced in Section 2.2, using atm for
the type of elements. Since the antecedents are atomic, only the initial and right
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

28

·

R. C. McDowell and D. A. Miller

rules are necessary:
seqI (A′ :: L) hAi
seqI L tt
seq(s I) L (B & C)
seq(s I) L (A ⇒ B)
V
seq(s I) L ( i B)

△

=
△
=
△
=
△
=
△
=

element A (A′ :: L)
⊤
seqI L B ∧ seqI L C
seqI (A :: L) B
∀i x seqI L (B x) .

We now turn to consider the set of definite clauses that make up the theory for the
derivation. Notice that the atomic formula A is equivalent
V
V to the formula tt ⇒ A, so
every definite clause can be written in the form x1 · · · xn (G ⇒ A). In addition,
the logic under consideration is a subset of the logic of hereditary Harrop formulas.
As a result, for any derivable sequent there is a uniform derivation of that sequent
[Miller 1990; Miller et al. 1991]. In our setting, a derivation is uniform if every
subderivation ending in a left rule is of the form
..
..
init
Γ −→ G[t1 , . . . , tn /x1 , . . . , xn ] A′ , Γ −→ A′
⇒L
(G ⇒ A)[t1 , . . . , tn /x1 , . . . , xn ], Γ −→ A′ V
L ,
V
V
′
x1 · · · xn (G ⇒ A), Γ −→ A

where A′ and A[t1 , . . . , tn /x1 , . . . , xn ] are the same. If we group these steps together,
our aggregate left
needs to say that seq(s I) L hA′ i holds if and only if
V rule encoding
V
there is a clause x1 · · · xn (G ⇒ A) in the theory such that A can be instantiated
to match A′ , and seqI L G′ holds, where G′ is the corresponding instantiation of
G. We use the predicate
prog : atm → prp → o

V
V
to encode the theory. The fact that the definite clause x1 · · · xn (G ⇒ A) is in
△
the theory is represented by the definitional clause prog A G = ⊤; the quantification
of the definite clause is encoded by the (elided) quantification of the definitional
clause. The encoding for the aggregate left rule is
△

seq(s I) L hAi = ∃b(prog A b ∧ seqI L b) ;
notice that the matching between A and the head of the definite clause is accomplished by the definition rules. Different object-level theories can be considered by
varying the definition of prog, as illustrated in Part III. The object-level formulas encoded using prog are treated by the object logic as a theory and not as a
definition: there is no rule corresponding to F Oλ∆IN ’s defL in the object logic.
We will refer to the six clauses for seq given in this section as D(intuit ). For
convenience we will abbreviate the formula ∃i(nat i ∧ seqi L B) as L ✄ B (or as ✄B
when L is nil). We now state the following properties about this presentation of the
object logic. If B is a term of type prp, then let h[B]i be its (obvious) translation
into a formula of intuitionistic logic. If L is a term of type atmlst, let h[L]i be its
(obvious) translation to a multiset of atomic formulas of intuitionistic logic.
Theorem 5.1 Adequacy of Encoding Intuitionistic Logic. Let D(prog )
△
△
be the definition {∀x̄1 [prog A1 G1 = ⊤], . . . , ∀x̄n [prog An Gn = ⊤]} (n ≥ 0) which
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

·

29

represents an object-level theory, andVlet P be the corresponding theory in intuitionistic logic (i.e., the set of formulas x̄i (h[Gi ]i ⇒ h[Ai ]i), for all i ∈ {1, . . . , n}). Let
D be a definition that extends D(nat ) ∪ D(list (atm)) ∪ D(intuit) ∪ D(prog) with
clauses that do not define nat, seq, element, or prog. Then the sequent −→ L ✄ B
is derivable in F Oλ∆IN with definition D if and only if h[B]i is an intuitionistic
consequence of h[L]i ∪ P.
Proof. The reverse direction follows easily from the definition D(intuit ). For
the forward direction, the use of the defR rule with D(intuit ) will cause the structure of the F Oλ∆IN derivation to closely follow that of the corresponding derivation
in intuitionistic logic. However, we need to be sure that the natL and defL rules
don’t allow us to derive anything that we can’t derive in intuitionistic logic. In fact,
we can show that a cut-free derivation of −→ L ✄ B will consist only of sequents
with empty antecedents [McDowell 1997]. Thus the natL and defL rules are not
used, since they both require a formula in the antecedent.
The following theorem states that we can derive in F Oλ∆IN that the specialization rule, the cut rule and the usual structural rules (exchange, weakening, and
contraction) are admissible for our object logic.
Theorem 5.2 Admissibility of Rules for Intuitionistic Object Logic.
The following formulas are derivable in F Oλ∆IN using the definition
D(nat ) ∪ D(list (atm)) ∪ D(intuit) :
Specialization Rule:
∀i∀b∀l(nat i ⊃ seq(s i) l

^

b ⊃ ∀x seqi l (b x))

Cut Rule:
∀a∀b∀l((a :: l) ✄ b ⊃ l ✄ hai ⊃ l ✄ b)
Structural Rules:
∀i∀b∀l∀l′ (nat i ⊃ ∀a(element a l ⊃ element a l′ ) ⊃ seqi l b ⊃ seqi l′ b)
5.2 Linear logic
Now consider the fragment of second-order linear logic given by the grammar
V
V
D ::= A | G −◦ A | G ⇒ A |
α x.D |
α→α
V x.D
G ::= A | tt | G & G | A −◦ G | A ⇒ G |
α x.G ,

where A ranges over atomic formulas and α ranges over ground types. As in
Section 5.1, D and G represent definite clauses and goal formulas, respectively.
The constants encoding these connectives have the same types as the corresponding
constants used in Section 5.1; the new constant −◦ has type atm → prp → prp.
We again separate the antecedents of sequents in a derivation into a theory, which
remains constant throughout the derivation and is encoded via a predicate prog,
and some atomic antecedents, which vary from sequent to sequent in the derivation
and are shown explicitly in the sequent. The atomic antecedents are further divided
into linear and intuitionistic antecedents:
seq : nt → (evs → atmlst) → (evs → atmlst) → (evs → prp) → o .
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

30

·

R. C. McDowell and D. A. Miller

Table IX.

Explicit eigenvariable encoding of lists
△

length nil∗ z = ⊤
△

length (A ::∗ L) (s I) = length L I
△

list L = ∃i(nat i ∧ length L i)
△

element A (A ::∗ L) = ⊤
△

element A (A′ ::∗ L) = element A L
△

split nil∗ nil∗ nil∗ = ⊤
△

split (A ::∗ L1 ) (A ::∗ L2 ) L3 = split L1 L2 L3
△

split (A ::∗ L1 ) L2 (A ::∗ L3 ) = split L1 L2 L3
△

permute nil∗ nil∗ = ⊤
△

permute (A ::∗ L1 ) L2 = ∃l22 (split L2 (A ::∗ nil∗ ) l22 ∧ permute L1 l22 )

The second and third arguments to seq represent multisets of intuitionistic and
linear antecedents, respectively. Notice that we follow the explicit eigenvariable
encoding style of Section 4.4 by encoding the antecedents and consequent as functions whose domain is a list of eigenvariables. We could use the explicit sequent
technique to encode linear logic and still prove the adequacy and admissibility theorems of this section. However, in Part III we will use the linear logic encoding
of this section as a specification logic; the proof of the unicity of typing theorem
in Section 9 uses meta-theoretic analysis that is not possible if we use the explicit
sequent technique here. This also gives us the opportunity to provide a detailed
illustration of the explicit eigenvariable encoding style. In order to highlight both
the similarities and differences between our current encoding and the encoding of
Section 5.1, we will use a number of abbreviations; we introduce the first of these
now. For any type τ , we will use τ ∗ as an abbreviation for evs → τ . Thus the type
of seq above can be expressed as
seq : nt → atmlst∗ → atmlst∗ → prp∗ → o .
We must modify the definition D(list (τ )) from Section 2.2 to work over the type
lst∗ . The predicates will now have the following types:
length : lst∗ → nt → o
list : lst∗ → o
element : τ ∗ → lst∗ → o .

split : lst∗ → lst∗ → lst∗ → o
permute : lst∗ → lst∗ → o

The new definition D(list ∗ (τ )) is shown in Table IX; we use nil∗ and A ::∗ L as
abbreviations for λl nil and λl ((A l) :: (L l)).
We similarly introduce abbreviations corresponding to constructors of prp∗ : hAi∗
abbreviates λl hA li, tt∗ abbreviates λl tt, B &∗ C abbreviates λl ((B l) & (C l)),
∗
A −◦∗ B abbreviates λl
V
V((A l) −◦ (B l)), A ⇒ B abbreviates λl ((A l) ⇒ (B l)), and
∗
B abbreviates λl ( x(B l x)).
Any definite clause in our fragment of linear logic is equivalent to a formula of
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

Table X.

·

31

Explicit eigenvariable encoding of linear logic
△

seqI IL (A ::∗ nil∗ ) hAi∗ = ⊤
△

∗

seqI (A′ ::∗ IL) nil hAi∗ = element hAi∗ (A′ ::∗ IL)
△

seq(s I) IL LL hAi∗ = ∃ll∃il (list ll ∧ list il ∧ prog A ll il ∧
split seqI IL LL ll ∧ split seqI IL nil∗ il)
△

seqI IL LL tt∗ = ⊤
△

&∗

seq(s I) IL LL (B
C) = seqI IL LL B ∧ seqI IL LL C
△
seq(s I) IL LL (A −◦∗ B) = seqI IL (A ::∗ LL) B
△

seq(s I) IL LL (A ⇒∗ B) = seqI (A ::∗ IL) LL B

V∗

seq(s I) IL LL (

i

△

B) = seqI (λl IL (rst l)) (λl LL (rst l)) (λl B (rst l) (fsti l))
△

split seqI IL nil∗ nil∗ = ⊤
△

split seqI IL LL (B ::∗ L) = ∃ll1 ∃ll2 (split LL ll1 ll2 ∧
seqI IL ll1 B ∧ split seqI IL ll2 L)

the form
^

x1 · · ·

^

xk (B1 ⇒ · · · Bm ⇒ C1 −◦ · · · Cn −◦ A) ,

for some k, m, n ≥ 0 and goal formulas B1 , . . . , Bm , C1 , . . . , Cn . Uniform derivations
have also been shown to be complete for this logic [Hodas and Miller 1994]; thus
we use the predicate
prog : atm∗ → prplst∗ → prplst∗ → o
to encode the set of definite clauses that make up the theory. The first argument
represents the atomic head of the definite clause; the second and third arguments
represent the lists C1 , . . . , Cn of linear hypotheses and B1 , . . . , Bm of intuitionistic
hypotheses, respectively. The quantification of the definite clause is again encoded
by the (elided) quantification of the corresponding definitional clause for prog.
Notice that the quantified variables of the definitional clause should be able to
match terms containing object-level eigenvariables and so should have type i∗ (for
first-order variables) or (i → i)∗ (for second-order variables). On the other hand,
the definite clause itself should be closed, so the constants fstτ and rst (used to
encode eigenvariables) should not occur in the corresponding definitional clause.
The predicate
split seq : nt → atmlst∗ → atmlst∗ → prplst∗ → o
will be used to express the idea that the propositions in the last argument are
derivable from the intuitionistic and linear antecedents in the second and third
arguments. Each linear antecedent must be used exactly once in the derivation of
all propositions in the last list.
The inference rules for this logic are encoded in the definition D(linear ) of Table X, which defines the predicates seq and split seq. The third clause in the definition says that an atomic formula A is derivable from intuitionistic antecedents
IL and linear antecedents LL if there is a definite clause in the object-level theory
whose head is A, whose linear hypotheses are derivable from the antecedents IL
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

32

·

R. C. McDowell and D. A. Miller

and LL, and whose intuitionistic hypotheses are derivable from the antecendents
IL. The other definitional clauses in Table X are similar to those in the explicit
eigenvariable encoding of intuitionistic logic given inVSection 4.4, but modified to
reflect the linearity constraints. In the clause for i we subscript the constant
fst with the type i because we also need a constant fsti→i : evs → i → i for the
representation of second-order eigenvariables in definite clauses. As in the previous
section, different object-level theories can be considered by varying the definition
of prog; an example theory will be given in Part III. For convenience we will abbreviate the formula ∃i(nat i ∧ seqi IL LL B) as IL; LL ✄ B (or as ✄B when IL
and LL are nil∗ ). If B is a term of type prp and L is a term of type atmlst, then
let h[B]i and h[L]i be their translations into a formula of linear logic and a multiset
of atomic formulas of linear logic, respectively.
Theorem 5.3 Adequacy of Encoding Linear Logic. Fix a F Oλ∆IN signature whose only constants with types involving evs are fsti , fsti→i , and rst. Let
D(prog ) be the definition
△

△

{∀ȳ1 [prog A1 LL1 IL1 = ⊤], . . . , ∀ȳn [prog An LLn ILn = ⊤]}
(n ≥ 0), where the quantified variables in the list ȳi each have type i∗ or (i → i)∗ ,
and the constants fstτ and rst do not occur in Ai , LLi , or ILi , for all i ∈ {1, . . . , n}.
Let P be the theory in linear logic that corresponds to D(prog), and let D be a
definition that extends D(nat ) ∪ D(list ∗ (atm)) ∪ D(list ∗ (prp)) ∪ D(linear ) ∪ D(prog )
with clauses that do not define nat, length, list, element, split, split seq, prog, or
seq. Finally, let IL: atmlst∗ , LL: atmlst∗ , and B: prp∗ be terms that do not contain
occurrences of the constant fsti→i . Then the sequent −→ IL; LL ✄ B is derivable
in F Oλ∆IN with definition D if and only if the sequent P, h[IL]i; h[LL]i −→ h[B]i is
derivable in linear logic.
Proof. We can restrict our attention to uniform derivations in linear logic,
since they are complete for this fragment of linear logic [Hodas and Miller 1994].
As before a cut-free derivation of −→ IL; LL ✄ B will consist only of sequents with
empty antecedents. Thus the definition of seq will ensure that the structure of the
F Oλ∆IN derivation will closely follow that of the corresponding derivation in linear
logic. The proof of the forward direction goes by induction on the structure of
the F Oλ∆IN derivation, and the reverse direction by induction on the structure of
the linear logic derivation. In general each case follows easily from the induction
hypothesis. A more detailed proof of this theorem, including a definition of the h[ ]i
translations, can be found in McDowell [1997].
We now present the theorems that we have derived in F Oλ∆IN about our object
logic. In order to express and prove these theorems, we need additional predicates
for operations related to the evs parameter. The predicates
subst : nt → i∗ → τ ∗ → τ ∗ → o
subst0 : nt → i∗∗ → τ ∗∗ → τ ∗∗ → o
will be used to represent substitution for eigenvariables; this is a simple generalization of the predicate of Section 4.4 to allow substitution in expressions of an
arbitrary type τ . The type τ ∗∗ should be understood to mean (τ ∗ )∗ , i.e., an abACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

Table XI.

·

33

Encoding of eigenvariable operations

△

subst I T X X ′ = subst0 I (λl′ T ) (λl′ X) (λl′ X ′ )
subst0 z T (λl′ λl X l′ (fst l) (rst l)) (λl′ λl X l′ (T l′ l) (rst l))
△

subst0

= ⊤
(s I)
(fst l) (rst l))
(λl′ λl X l′ (fst l) (rst l)) (λl′ λl X ′ l′ (fst l) (rst l))
(λl′ λl T l′

△

= subst0 I (λl′ λl T (rst l′ ) (fst l′ ) l)
(λl′ λl X (rst l′ ) (fst l′ ) l) (λl′ λl X ′ (rst l′ ) (fst l′ ) l)
△

extend evars I X X ′ = extend evars0 I (λl′ X) (λl′ X ′ )
extend evars0 z (λl′ λl X l′ l) (λl′ λl X l′ (rst l))
△

extend evars0

= ⊤
(s I) (λl′ λl X l′ (fst l) (rst l)) (λl′ λl X ′ l′ (fst l) (rst l))
△

= extend evars0 I (λl′ λl X (rst l′ ) (fst l′ ) l)
(λl′ λl X ′ (rst l′ ) (fst l′ ) l)

brevation for (evs → evs → τ ). We will also use the predicates
extend evars : nt → τ ∗ → τ ∗ → o
extend evars0 : nt → τ ∗∗ → τ ∗∗ → o
to add a new eigenvariable to the list at an offset. Thus extend evars i x x′
indicates that x′ is the result of adding a new eigenvariable in x at the (i + 1)th
position in the list; the eigenvariables that previously occupied positions (i + 1) or
greater are shifted to one position later in the list. These predicates are defined in
the definition D(evars(τ )) of Table XI. We will also need an version of D(list (τ ))
to work over the type lst∗∗ ; it is similar to D(list ∗ (τ )) and we will refer it as
D(list ∗∗ (τ )).
Since we want our theorems about the object logic to be independent of any
particular object logic theory, we need to include some assumptions about the
predicate prog. Specifically, we will need to know that if an atom matches the head
of a clause in the theory, then if we substitute for an eigenvariable in the atom or
extend the list of eigenvariables, then the resulting atom will still match the head
of the clause. We encode these assumptions as the following two formulas:
∀i∀t∀a∀a′ ∀ll∀il(nat i ⊃ prog a ll il ⊃ subst i t a a′ ⊃
∃ll′∃il′ (prog a′ ll′ il′ ∧ subst i t ll ll′ ∧ subst i t il il′ )) ,
which we will refer to as Psubst , and
∀i∀a∀a′ ∀ll∀il(nat i ⊃ prog a ll il ⊃ extend evars i a a′ ⊃
∃ll′∃il′ (prog a′ ll′ il′ ∧ extend evars i ll ll′ ∧ extend evars i il il′ )) ,
which we will refer to as Pextend . The theory should not contain occurrences of
eigenvariables, so the definition of prog should not contain occurrences of fst or rst.
If this is the case, then Psubst and Pextend will be derivable in F Oλ∆IN .
The following theorem states that we can derive in F Oλ∆IN that the specialization
rule, the cut rule, and the usual linear logic structural rules are admissible for our
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

34

·

R. C. McDowell and D. A. Miller

object logic. We refer to the definition
D(list ∗ (atm)) ∪ D(list ∗ (prp)) ∪ D(list ∗∗ (atm)) ∪ D(list ∗∗ (prp))
as D(lists) and the definition
D(evars(atm)) ∪ D(evars (prp)) ∪ D(evars (atmlst)) ∪ D(evars(prplst))
as D(evars).
Theorem 5.4 Rule Admissibility for Linear Logic. The formulas below
are derivable in F Oλ∆IN using the definition D(nat )∪D(lists )∪D(evars )∪D(linear ):
Specialization Rule:
Psubst ⊃
∀i∀b∀il∀ll(nat i ⊃ listV
il ⊃ list ll ⊃
∗
b ⊃ ∀x seqi il ll (b x))
seq(s i) il ll
Cut Rule:
Pextend ⊃
∀a∀b∀il∀ll(list il ⊃ list ll ⊃
(a ::∗ il); ll ✄ b ⊃ il; nil∗ ✄ hai∗ ⊃ il; ll ✄ b)
Structural Rules:
Pextend ⊃
∀a∀b∀il∀ll∀ll1∀ll2 (list il ⊃ list ll ⊃ split ll ll1 ll2 ⊃
il; (a ::∗ ll1 ) ✄ b ⊃ il; ll2 ✄ hai∗ ⊃ il; ll ✄ b)
∀i∀b∀il∀il′∀ll∀ll′(nat i ⊃ list il ⊃ list il′ ⊃ list ll ⊃
∀a(element a il ⊃ element a il′ ) ⊃ permute ll ll′ ⊃
seqi il ll b ⊃ seqi il′ ll′ b)
6. RELATED WORK
In this part of the paper we have presented several different encodings of logics; for
each we discussed the extent to which reasoning about the encoded logic can take
place within the meta-logic F Oλ∆IN . None of the encoding techniques is completely
original, but their ability to support formal meta-theoretic analysis is a relatively
new concern.
The natural deduction-style encoding of Section 4.1 is the prototypical representation style of higher-order abstract syntax. For example, the seminal paper
on the Edinburgh Logical Framework (LF) [Harper et al. 1993] encodes first-order
and higher-order logic in this manner and proves the adequacy of these encodings.
The issue of meta-theoretic analysis of the encodings within the meta-logic is not
addressed there.
The use of separate predicates for formulas on the left and right sides of the
sequent, as was done in Section 4.2, is also common. Pfenning [1995], for example, uses this representation style to encode structural cut-elimination proofs for
intuitionistic, classical, and linear logics. The induction cases of these proofs are
represented in Elf, so some amount of reasoning about the encoded logics is done
in the meta-logic. However Elf does not itself contain any support for induction, so
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

·

35

the completeness of the cases must be checked outside of the formal framework using techniques such as schema checking [Pfenning and Rohwedder 1992; Rohwedder
and Pfenning 1996]. Miller [1996] uses both this sequent style of encoding and the
natural deduction style. The two encodings are used to show that natural deduction
and sequent calculus presentations of minimal logic have the same theorems. The
proof of this result combines informal reasoning with formal reasoning in a linear
logic meta-logic.
Section 4.3 presented an encoding of logic which encoded the derivability of a
sequent in a single predicate. This style of encoding was used in an early paper on
the use of higher-order abstract syntax [Miller and Nadathur 1987]. That paper
focuses on an operational interpretation of such a specification, however, and does
not discuss the potential for reasoning about the encoded logic in the meta-logic.
The idea of representing free variables as a list, discussed in Section 4.4, was first
used in the context of higher-order abstract syntax by Despeyroux and Hirschowitz
[1994]. Their intent was to develop a way to use higher-order abstract syntax within
the setting of the inductive definition facility of Coq. A key difference between their
technique and ours is that they use both constructor and deconstructor operators
for lists in the context of an equality theory. The encoding of the right rule for
universal quantification in that setting might look like the following:
V
△
seq(s I) L (λl i x(B (cons x l))) = seqI (λl′ L(rst l′ )) B .

Within terms, bound and free variables are accessed by selecting the appropriate
element from the list. In our simpler setting (without an equality theory) we use
unification to get by with only deconstructors for variable lists. The paper Despeyroux and Hirschowitz [1994] was the first attempt to fully support formal reasoning
about higher-order abstract syntax encodings within a meta-logic. Their examples
involved encodings of simply-typed λ-terms, so we will discuss their work further
at the end of Part III.
Part III: OBJECT LOGICS AS SPECIFICATION LOGICS

In this part we consider reasoning about higher-order abstract syntax encodings of
programming languages. We could choose one of the representation strategies used
for logics in the previous part; instead we adopt a different strategy that allows us to
use the traditional higher-order abstract syntax representation to its full advantage
and still reason formally about the encoded system. The key to accomplishing
this is to not specify the programming language directly in F Oλ∆IN , but in a small
object logic that is itself specified in F Oλ∆IN . In this way we can reason in F Oλ∆IN
about the structure of object logic sequents and their derivability.
The use of object-level sequents may seem at first a rather drastic step to take
to embed the kind of hypothetical judgements common with higher-order abstract
syntax into a meta-logic. Such a representation is, however, used in various areas
of programming language semantics. For example, Mitchell, in his textbook [1995],
uses typing judgements of the form Γ ✄ M : σ and performs induction over their
(sequent-style) derivation. This separation of the (object) specification logic from
the meta-logic (F Oλ∆IN ) in which reasoning is performed also reflects the usual
structure of informal reasoning about higher-order abstract syntax encodings.
In the next section we motivate this approach through an informal proof of subACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

36

·

R. C. McDowell and D. A. Miller

ject reduction for the untyped λ-calculus. We proceed in Section 8 to formalize this
proof by encoding the static and dynamic semantics for untyped λ-terms in the
intuitionistic object logic of Section 5.1. We also list a variety of other theorems
about the language that we have derived in F Oλ∆IN . The remainder of the section extends the encoding to the Programming language of Computable Functions
(PCF) [Scott 1969]. In Section 9 we consider an encoding of PCF with references
(PCF:= ) [Gunter 1992] in the linear object logic of Section 5.2. Finally, Section 10
compares the framework of this part with other research in formal reasoning about
higher-order abstract syntax encodings.
7. MOTIVATION FROM INFORMAL REASONING
In order to motivate our framework for reasoning about higher-order abstract syntax encodings, we consider a specification in intuitionistic logic of call-by-name
evaluation and simple typing for the untyped λ-calculus. We introduce two types,
tm and ty, to denote object-level terms and types. To represent the untyped λterms we introduce the two constants abs of type (tm → tm) → tm and app of
type tm → tm → tm to denote object-level abstraction and application, respectively. Object-level types will be built up from a single primitive type using the
arrow type constructor; these are denoted in the specification logic by the constants
gnd of type ty and arr of type ty → ty → ty.
To specify call-by-name evaluation, we use an infix predicate ⇓ of type tm →
tm → o and the two formulas
V
r((abs r) ⇓ (abs r))
V V V V
m n v r((m ⇓ (abs r) & (r n) ⇓ v) ⇒ (app m n) ⇓ v) .
To specify simple typing at the object-level, we use the binary predicate typeof
of type tm → ty → o and the two formulas
V V V V
V mV n
V tV u((typeof m (arr u t) & typeof n u) ⇒ typeof (app m n) t)
r t u( x(typeof x t ⇒ typeof (r x) u) ⇒ typeof (abs r) (arr t u)) .

Proofs that these two predicates correctly capture the notions of call-by-name evaluation and of simple typing can be found in various places in the literature: see,
for example, Avron et al. [1992] and Hannan [1990].
Now consider the following subject reduction theorem and its proof. We use ⊢
here to represent derivability in intuitionistic logic from the above formulas encoding
evaluation and typing; we omit displaying these formulas on the left of the turnstile
to simplify the presentation.
Proposition 7.1. If ⊢ P ⇓ V and ⊢ typeof P T , then ⊢ typeof V T .

Proof. We prove this theorem by induction on the height of the derivation of
P ⇓ V . Since P ⇓ V is atomic, its derivation must end with the use of one of the formulas encoding evaluation. If the ⇓ formula for abs is used, then P and V are both
equal to abs R, for some R, and the consequent is immediate. If P ⇓ V was derived
using the ⇓ formula for app, then P is of the form (app M N ), and for some R there
are shorter derivations of M ⇓ (abs R) and (R N ) ⇓ V . Since P is (app M N ),
typeof P T must have been derived using the formula encoding the typing rule for
app. Hence, there is a U such that ⊢ typeof M (arr U T ) and ⊢ typeof N U . Applying the inductive hypothesis to the evaluation and typing judgements for M , we
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

·

37

have ⊢ typeof (abs R) (arr U T ). This atomic
V formula must have been derived using
the typeof formula for abs, and, hence, ⊢ x(typeof x U ⇒ typeof (R x) T ). Since
our specification logic is intuitionistic logic, we can instantiate this quantifier with
N and use cut and cut-elimination to conclude that ⊢ typeof (R N ) T . Applying
the inductive hypothesis to the judgements for (R N ) yields ⊢ typeof V T .
This proof is clear and natural, and we would like to be able to formally capture
proofs quite similar to this in structure. This suggests that the following features
would be valuable in our framework:
(1) Two distinct logics. One of the logics would correspond to the one written
with logical syntax above and would capture judgements, e.g., about typability and
evaluation. The second logic would represent a formalization of the English text
in the proof above. Atomic formulas of this second (meta-) logic would encode
judgements in the first (object) logic.
(2) Induction over at least natural numbers.
(3) Instantiation of meta-level eigenvariables. In the proof above, for example,
the meta-level variable P was instantiated in one part of the proof to (abs R)
and in another part of the proof to (app M N ). Notice that this instantiation of
eigenvariables within a proof does not happen in a strictly intuitionistic sequent
calculus.
(4) Analysis of the derivation of an assumed judgement. In the proof above this
was done a few times, leading, for example, from the assumption
⊢ typeof (abs R) (arr U T )
to the assumption
⊢

^

x(typeof x U ⇒ typeof (R x) T ) .

The specification of typeof allows the implication to go in the other direction, but
given the structure of the specification of typeof, this direction can also be justified
at the meta-level.
In our framework, we accommodate the first feature by specifying an object logic
within the meta-logic F Oλ∆IN , as illustrated in Part II. The natL rule of F Oλ∆IN
provides natural number induction. The last two features are accommodated by
the definition facilities of F Oλ∆IN , in particular the defL rule. We demonstrate our
approach in the remaining sections of the paper, beginning with a formalization of
the example from this section.
8. REPRESENTATION AND ANALYSIS OF A FUNCTIONAL PROGRAMMING
LANGUAGE
8.1 The language of untyped λ-terms
We first demonstrate our approach to formal reasoning about higher-order abstract
syntax encodings using the example of untyped λ-terms. This encoding will be
similar to the one used to motivate the framework in the preceding section. The
object logic used will be the fragment of second-order intuitionistic logic encoded
by the definition D(intuit ) of Section 5.1.
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

38

·

R. C. McDowell and D. A. Miller

Table XII.

Object logic encoding of typing and evaluation of untyped λ-terms

V

prog (typeof (abs R) (arr T U ))
n((typeof n T ) ⇒ htypeof (R n) U i)
prog (typeof (app M N ) T )
htypeof M (arr U T )i & htypeof N U i
prog ((abs R) ⇓ (abs R))
prog ((app M N ) ⇓ V )

tt
hM ⇓ (abs R)i & h(R N ) ⇓ V i

prog ((app (abs R) M ) ❀ (R M ))
prog ((app M N ) ❀ (app M ′ N ))
prog (M ❀∗ M )
prog (M ❀∗ N )

tt
hM ❀ M ′ i

tt
hM ❀ M ′ i & hM ′ ❀∗ N i

The required constants to represent λ-terms are abs : (itm → itm ) → itm and
app : itm → itm → itm ; for simple types (over one primitive type) we need gnd: ity
and arr: ity → ity → ity . Since both types and terms in the language are represented by the object logic type i, we have added subscripts tm and ty. These
subscripts should not be considered part of the encoding, but are added to improve
the readability of these declarations.
Our object logic predicate representing typability is denoted by the F Oλ∆IN
constant typeof of type itm → ity → atm. The predicates for natural semantics
and transition semantics are denoted by the constants ⇓, ❀, and ❀∗ , all of type
itm → itm → atm. The object logic specifications for these are the usual ones,
written in the Lλ subset of higher-order logic [Miller 1991] and are those common to specifications written in, say, λProlog [Hannan and Miller 1992] and Elf
[Pfenning 1989]. This object-level specification is represented in F Oλ∆IN as the
△
definition D(lambda) shown in Table XII. (We have dropped the = ⊤ body of
these clauses.) This definition can be interpreted in a logic programming fashion
to compute object-level simple type checking and call-by-name evaluation in both
structural operational semantic and natural semantic styles. Call-by-value is just
as easily represented and used.
The following theorem lists the properties of the untyped λ-calculus that we
have derived in F Oλ∆IN : determinacy of semantics, equivalence of semantics, and
subject reduction. The F Oλ∆IN derivations closely follow the informal proofs of
these properties.
Theorem 8.1. The following formulas are derivable in F Oλ∆IN from the definition that accumulates D(nat ), D(list (atm)), D(intuit ), D(lambda) and the clause
△
X ≡ X = ⊤ defining the predicate ≡: i → i → o.
Determinacy of semantics:
∀m∀m1 ∀m2 (✄hm ⇓ m1 i ⊃ ✄hm ⇓ m2 i ⊃ m1 ≡ m2 )
∀m∀m1 ∀m2 (✄hm ❀ m1 i ⊃ ✄hm ❀ m2 i ⊃ m1 ≡ m2 )
∀m∀r1 ∀r2 (✄hm ❀∗ (abs r1 )i ⊃ ✄hm ❀∗ (abs r2 )i ⊃ (abs r1 ) ≡ (abs r2 ))
Equivalence of semantics:
∀m∀r(✄hm ⇓ (abs r)i ⊃ ✄hm ❀∗ (abs r)i)
∀m∀r(✄hm ❀∗ (abs r)i ⊃ ✄hm ⇓ (abs r)i)
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

·

39

Subject reduction:
∀m∀n(✄hm ⇓ ni ⊃ ∀t(✄htypeof m ti ⊃ ✄htypeof n ti))
∀m∀n(✄hm ❀ ni ⊃ ∀t(✄htypeof m ti ⊃ ✄htypeof n ti))
∀m∀n(✄hm ❀∗ ni ⊃ ∀t(✄htypeof m ti ⊃ ✄htypeof n ti))
Proof. We show the derivation of the first subject reduction property, which is
a formalization of Proposition 7.1.
We wish to show that evaluation preserves types:
−→ ∀p∀v(✄hp ⇓ vi ⊃ ∀t(✄htypeof p ti ⊃ ✄htypeof v ti)) .
(We have changed the names of the quantified variables to agree with those in the
informal proof.) Applying the ∀R, ⊃ R, ∃L, cL, and ∧L rules to the above sequent
yields
nat i, seqi nil hp ⇓ vi, ✄htypeof p ti −→ ✄htypeof v ti .
(Recall that ✄hp ⇓ vi is an abbreviation for ∃i(nat i ∧ seqi nil hp ⇓ vi).)
As in the informal proof, we proceed with an induction on the height of the
derivation of p ⇓ v, which is represented here by i. We will use the derived rule for
complete induction (Proposition 2.3) and our induction predicate will be
λi∀p∀v∀t(seqi nil hp ⇓ vi ⊃ ✄htypeof p ti ⊃ ✄htypeof v ti) ,
which we will denote by IP. The derivation of the conclusion from the induction
predicate applied to i is trivial, so it only remains to derive the induction step
nat j, ∀k(nat k ⊃ k < j ⊃ (IP k)) −→ (IP j) .
We use the ∀R and ⊃ R rules to obtain
nat j, ∀k . . . , seqj nil hp ⇓ vi, ✄htypeof p ti −→ ✄htypeof v ti .
In the informal proof we use the fact that the derivation of the atomic formula
p ⇓ v must end with the use of a clause from the specification of evaluation. We
deduce this formally by applying the defL rule to seqj nil hp ⇓ vi, which yields
nat (s j0 ), ∀k . . . , ∃b(prog (p ⇓ v) b ∧ seqj0 nil b), ✄htypeof p ti −→ ✄htypeof v ti .
We next apply the ∃L, cL, and ∧L rules, and then apply the defL rule to prog (p ⇓
v) b which yields the two sequents
nat (s j0 ), ∀k . . . , seqj0 nil tt, ✄htypeof (abs r) ti −→ ✄htypeof (abs r) ti
nat (s j0 ), ∀k . . . , seqj0 nil hm ⇓ (abs r)i & h(r n) ⇓ vi,
✄htypeof (app m n) ti−→ ✄htypeof v ti .
This use of the defL rule corresponds to the case analysis of the formula used to
derive p ⇓ v. As in the informal case, the abs case (represented here by the first
sequent) is immediate. The derivation of the second sequent, representing the app
case, begins with the use of the defL, cL, and ∧L, bringing us to the sequent
nat (s2 j1 ), ∀k . . . , seqj1 nil hm ⇓ (abs r)i, seqj1 nil h(r n) ⇓ vi,
✄htypeof (app m n) ti−→ ✄htypeof v ti .
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

40

·

R. C. McDowell and D. A. Miller

(We use the term s2 j1 as an abbreviation for s (s j1 ).)
The informal proof continues with an analysis of the derivation of
typeof (app m n) t .
Again we accomplish this through two uses of the defL rule, the first to indicate
that the derivation must end with the use of a specification clause, and the second
to determine the applicable clauses. In this case there is only one applicable clause,
so we are left to derive the sequent
. . . , nat (s j0′ ), seqj0′ nil htypeof m (arr u t)i & htypeof n ui −→ ✄htypeof v ti .
Additional uses of the defL, cL and ∧L rules bring us to the sequent
. . . , nat (s2 j1′ ), seqj1′ nil htypeof m (arr u t)i,
seqj1′ nil htypeof n ui−→ ✄htypeof v ti .
In the informal proof we now apply the induction hypothesis to the evaluation
and typing judgments for m. We accomplish this here by applying the appropriate
left rules to the elided induction hypothesis ∀k . . .. This requires the derivation of
the five sequents
nat (s2 j1 ), . . . −→ nat j1

nat (s2 j1 ), . . . −→ j1 < (s2 j1 )

. . . , seqj1 nil hm ⇓ (abs r)i, . . . −→ seqj1 nil hm ⇓ (abs r)i
. . . , nat (s2 j1′ ), seqj1′ nil htypeof m (arr u t)i, . . . −→ ✄htypeof m (arr u t)i
nat (s2 j1 ), ∀k . . . , seqj1 nil h(r n) ⇓ vi,
✄htypeof (abs r) (arr u t)i,
nat (s2 j1′ ), seqj1′ nil htypeof n ui−→ ✄htypeof v ti .
The first two of these represent the fact that the measure of the evaluation derivation for m is a natural number that is smaller than the measure of the original
evaluation derivation for p. By Proposition 2.4 these are derivable in F Oλ∆IN from
D(nat ). The third sequent is immediate, and the fourth also follows easily from
Proposition 2.4.
The derivation of the fifth sequent proceeds with another two applications of the
defL rule, corresponding to the analysis of the proof of typeof (abs r) (arr u t) in
the informal proof. This yields the sequent
V
. . . , nat (s j0′′ ), seqj0′′ nil x((typeof x u) ⇒ htypeof (r x) ti),
. . .−→ ✄htypeof v ti .
This is followed by applications of the defL and ∀L rules to give us
. . . , nat (s3 j1′′ ), seqj1′′ ((typeof n u) :: nil) htypeof (r n) ti, . . . −→ ✄htypeof v ti .
The informal proof proceeds with a use of the cut rule, and here we use the derived
object-level cut rule (Theorem 5.2) with the elided assumption seqj1′ nil htypeof n ui
to obtain
. . . , nat (s3 j1′′ ), seqj1′′ ((typeof n u) :: nil) htypeof (r n) ti,
. . . −→ ((typeof n u) :: nil) ✄ htypeof (r n) ti
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

·

41

. . . , nat (s2 j1′ ), seqj1′ nil htypeof n ui −→ ✄htypeof n ui
. . . , ✄htypeof (r n) ti −→ ✄htypeof v ti .
The first two of these follow easily from Proposition 2.4.
The informal proof concludes by applying the induction hypothesis to the evaluation and typing judgments for (r n). Again we accomplish this by applying the
appropriate left rules to the induction hypothesis ∀k . . ., which requires the derivation of the five sequents
nat (s2 j1 ) −→ nat j1

nat (s2 j1 ) −→ j1 < (s2 j1 )

. . . , seqj1 nil h(r n) ⇓ vi, . . . −→ seqj1 nil h(r n) ⇓ vi
. . . , ✄htypeof (r n) ti −→ ✄htypeof (r n) ti
. . . , ✄htypeof v ti −→ ✄htypeof v ti .
The first two sequents follow from Proposition 2.4, and the last three are all immediate.
8.2 A language for computable functions
We now extend the encoding of the static and dynamic semantics for untyped λterms from the previous section to the programming language PCF [Scott 1969].
The necessary F Oλ∆IN constants for PCF types are
num : ity

bool : ity

arr : ity → ity → ity .

Those for PCF terms are
zero : itm
true : itm
false : itm

succ : itm → itm
pred : itm → itm
is zero : itm → itm

if
abs
app
rec

:
:
:
:

itm → itm → itm → itm
ity → (itm → itm ) → itm
itm → itm → itm
ity → (itm → itm ) → itm .

We have again labeled the type i with subscripts to improve the readability of these
declarations. The first argument to abs and rec represent the PCF type tag for the
variable bound by the abstraction and recursion constructs.
The object logic predicates representing typability and evaluation are denoted
by the same F Oλ∆IN constants as in Section 8.1, plus the additional constant
value : itm → atm. The object-level specification is represented in F Oλ∆IN as the
definition D(PCF) shown in Tables XIII, XIV, and XV; we have again omitted
△
the = ⊤ body of the clauses. The following theorem lists the properties of PCF
that we have derived in F Oλ∆IN . The type tags in PCF terms allow the unicity of
typing to hold in addition to the determinacy of semantics, equivalence of semantics
and subject reduction. The F Oλ∆IN derivations again closely follow the informal
proofs of these properties; the only exception is the derivation of the unicity of
typing property, which we discuss below.
Theorem 8.2. The following formulas are derivable in F Oλ∆IN from the definition that accumulates D(nat ), D(list (atm)), D(intuit ), D(PCF) and the clause
△
X ≡ X = ⊤ defining the predicate ≡: i → i → o.
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

42

·

R. C. McDowell and D. A. Miller

Table XIII.
prog
prog
prog
prog
prog
prog
prog
prog
prog
prog

(typeof
(typeof
(typeof
(typeof
(typeof
(typeof
(typeof
(typeof
(typeof
(typeof

Object logic encoding of typing for PCF

zero num)
tt
true bool)
tt
false bool)
tt
(succ M ) num)
htypeof M numi
(pred M ) num)
htypeof M numi
htypeof M numi
(is zero M ) bool)
(if M N1 N2 ) T )
htypeof
V M booli & htypeof N1 T i & htypeof N2 T i
(abs T R) (arr T U ))
n((typeof n T ) ⇒ htypeof (R n) U i)
(app M N ) T )
Vhtypeof M (arr U T )i & htypeof N U i
(rec T R) T )
n((typeof n T ) ⇒ htypeof (R n) T i)

Table XIV.
prog
prog
prog
prog
prog
prog
prog
prog
prog
prog
prog
prog
prog

Object logic encoding of natural semantics for PCF

(zero ⇓ zero)
tt
(true ⇓ true)
tt
(false ⇓ false)
tt
((succ M ) ⇓ (succ V ))
hM ⇓ V i
((pred M ) ⇓ zero)
hM ⇓ zeroi
((pred M ) ⇓ V )
hM ⇓ (succ V )i
((is zero M ) ⇓ true)
hM ⇓ zeroi
hM ⇓ (succ V )i
((is zero M ) ⇓ false)
((if M N1 N2 ) ⇓ V )
hM ⇓ truei & hN1 ⇓ V i
((if M N1 N2 ) ⇓ V )
hM ⇓ falsei & hN2 ⇓ V i
((abs T R) ⇓ (abs T R))
tt
((app M N ) ⇓ V )
hM ⇓ (abs T R)i & h(R N ) ⇓ V i
((rec T R) ⇓ V )
h(R (rec T R)) ⇓ V i

Determinacy of semantics:
∀m∀m1 ∀m2 (✄hm ⇓ m1 i ⊃ ✄hm ⇓ m2 i ⊃ m1 ≡ m2 )
∀m∀m1 ∀m2 (✄hm ❀ m1 i ⊃ ✄hm ❀ m2 i ⊃ m1 ≡ m2 )
∀m∀v1 ∀v2 (✄hvalue v1 i ⊃ ✄hm ❀∗ v1 i ⊃ ✄hvalue v2 i ⊃ ✄hm ❀∗ v2 i ⊃ v1 ≡ v2 )
Equivalence of semantics:
∀m∀v(✄hm ⇓ vi ⊃ (✄hvalue vi ∧ ✄hm ❀∗ vi))
∀m∀v((✄hvalue vi ∧ ✄hm ❀∗ vi) ⊃ ✄hm ⇓ vi)
Subject reduction:
∀m∀n(✄hm ⇓ ni ⊃ ∀t(✄htypeof m ti ⊃ ✄htypeof n ti))
∀m∀n(✄hm ❀ ni ⊃ ∀t(✄htypeof m ti ⊃ ✄htypeof n ti))
∀m∀n(✄hm ❀∗ ni ⊃ ∀t(✄htypeof m ti ⊃ ✄htypeof n ti))
Unicity of typing:
∀m∀t1 ∀t2 (✄htypeof m t1 i ⊃ ✄htypeof m t2 i ⊃ t1 ≡ t2 )
The usual informal proof of the unicity of typing relies on the requirement that
the list of assumptions in the object logic sequent contains typing assignments only
for variables and no more than one assignment for any particular variable. Since we
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

Table XV.
prog
prog
prog
prog
prog
prog
prog
prog
prog
prog
prog
prog
prog

43

Object logic encoding of transition semantics for PCF
((succ M ) ❀ (succ M ′ ))
hM ❀ M ′ i
((pred zero) ❀ zero)
tt
((pred (succ V )) ❀ V )
hvalue V i
((pred M ) ❀ (pred M ′ ))
hM ❀ M ′ i
tt
((is zero zero) ❀ true)
((is zero (succ V )) ❀ false)
hvalue V i
hM ❀ M ′ i
((is zero M ) ❀ (is zero M ′ ))
((if true M N ) ❀ M )
tt
((if false M N ) ❀ N )
tt
((if M N1 N2 ) ❀ (if M ′ N1 N2 ))
hM ❀ M ′ i
((app (abs T R) N ) ❀ (R N ))
tt
((app M N ) ❀ (app M ′ N ))
hM ❀ M ′ i
((rec T R) ❀ (R (rec T R)))
tt

prog (M ❀∗ M )
prog (M ❀∗ N )
prog
prog
prog
prog
prog

·

(value
(value
(value
(value
(value

tt
(hM ❀ M ′ i & hM ′ ❀∗ N i)

zero)
tt
true)
tt
false)
tt
(succ V ))
(abs T R))

hvalue V i
tt

have encoded the variables of PCF as variables of our object logic, which in turn are
encoded as variables of F Oλ∆IN , we cannot state the first part of this requirement
in F Oλ∆IN . Thus our derivation (given in McDowell [1997]) must differ from the
informal proof. In fact, we make essential use of the PCF recursion construct in
the abs case of the derivation; for an arbitrary type u, the term (rec u (λy y)) has
the type u and no other type. As a result, our derivation does not generalize to
languages without this construct. In the next section we give an encoding of an
extension of PCF in the object logic of Section 5.2, which is encoded in F Oλ∆IN
using the explicit eigenvariable encoding. Although this explicit eigenvariable encoding makes the syntax more cumbersome, it allows the derivations in F Oλ∆IN to
be more natural. This is illustrated by the fact that we can capture in F Oλ∆IN the
typical proof of the unicity of typing.
9. REPRESENTATION AND ANALYSIS OF AN IMPERATIVE PROGRAMMING
LANGUAGE
In this section we consider the programming language PCF:= , an extension of PCF
with state [Gunter 1992]. This language extends PCF with reference types and
constructs for referencing, dereferencing, assignment, and sequential evaluation.
The type (refty τ ) is the type of references to values of type τ . If m is a term of
type τ , then (ref m) has type (refty τ ) and evaluates to a new memory location
containing the value of m. If m is a term of type (refty τ ), then the value of m is a
memory location, and !m has type τ and evaluates to the contents of that location.
If m has type (refty τ ) and n has type τ , then (m := n) has type τ . The evaluation
of (m := n) changes the contents of the value of m to be the value of n; its value is
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

44

·

R. C. McDowell and D. A. Miller

the same as the value of n. If m1 and m2 have types τ1 and τ2 , respectively, then
(m1 ; m2 ) has type τ2 . To evaluate (m1 ; m2 ), we first evaluate m1 , then evaluate
m2 , and finally return the value of m2 . Clearly the value of a PCF:= term will
depend on the state in which it is evaluated, and the state may be modified in the
evaluation process; thus evaluation becomes a mapping from a term-state pair to a
value-state pair.
To encode PCF:= , we use the linear object logic of Section 5.2, since linear
logic is well-suited as a specification logic for programming languages with state
[Cervesato and Pfenning 1996; Chirimar 1995; Miller 1996]. For such languages,
the order of evaluation becomes important, and so a continuation-based operational
semantics is often used for the encoding. In a continuation-based semantics, each
rule has at most one premise, and any additional evaluation steps are encoded
in the continuation. This encoding of the evaluation steps into the continuation
makes the order of evaluation explicit. A continuation-based semantics for PCF:= is
given in Table XVI; following Gunter [1992] we specify call-by-value evaluation. To
abbreviate our presentation we omit the rules for the natural number, boolean, and
conditional constructs; a presentation with the full language is given in McDowell
[1997]. The semantics of Table XVI and their object logic encoding given below
are a variation of those found in Cervesato and Pfenning [1996]. The judgement
κ ⊢ (M, σ) ֒→ φ represents the idea that the evaluation of the term M in state σ
with continuation κ results in the final answer φ. A continuation is a list whose
elements are of the form x̂.M , where M is a term containing the variable x. (We
use x̂ instead of λx to avoid confusion with λ-abstraction in PCF:= .) The answer φ
˙
is a pair including the final value and the final state. The judgement κ ⊢ (V, σ)֒→φ
indicates that passing the value V with state σ to the continuation κ results in the
final answer φ. In the rules of Table XVI, c is used to range over locations (reference
cells). In the rule for the continuation (x̂.ref x, κ), c must be a new location, i.e.,
a location that does not occur in the state σ. The expression σ[c 7→ V ] represents
the state that is the same as σ except that location c contains the value V .
To encode PCF:= , we use the constants
refty : ity → ity
cell : ilc → itm

ref : itm → itm
deref : itm → itm

assign : itm → itm → itm
sequence : itm → itm → itm

in addition to the constants of Section 8.2. Once again we have labeled the type i
with subscripts to improve the readability of these declarations. The subscript lc
indicates that the argument to cell represents a PCF:= location.
The object logic predicate representing typability is denoted by the same F Oλ∆IN
constants as in Section 8; its object-level specification is represented in F Oλ∆IN as
the definition shown in Table XVII. Recall that prog A (C1 :: . . . Cn :: nil) (B1 ::
. . . Bm :: nil) represents the definite clause
^
x̄(B1 ⇒ · · · Bm ⇒ C1 −◦ · · · Cn −◦ A) ,
where the free variables of A, B1 , . . . , Bm , C1 , . . . , Cn are included in the list x̄.
This means that to derive an instance of A, we can instead derive the corresponding
instances of B1 , . . . , Bm , C1 , . . . , Cn . To establish IL; LL ✄ hAi, the rules of linear
logic require that each assumption in LL be used exactly once in the derivation of
one of the Ci ’s; it cannot be used in the derivation of any of the Bi ’s, or in the
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

Table XVI.

·

Continuation-based natural semantics for PCF:=
x̂.ref x, κ ⊢ (M, σ) ֒→ φ

x̂.!x, κ ⊢ (M, σ) ֒→ φ

κ ⊢ (ref M, σ) ֒→ φ

κ ⊢ (!M, σ) ֒→ φ

˙
⊢ (V, σ)֒→(V,
σ)
˙
κ ⊢ (c, σ)֒→φ

˙
κ ⊢ (c, σ[c 7→ V ])֒→φ

˙
κ ⊢ (σ(c), σ)֒→φ

κ ⊢ (c, σ) ֒→ φ

˙
x̂.ref x, κ ⊢ (V, σ)֒→φ

˙
x̂.!x, κ ⊢ (c, σ)֒→φ

x̂.x := N, κ ⊢ (M, σ) ֒→ φ

x̂.V := x, κ ⊢ (N, σ) ֒→ φ
˙
x̂.x := N, κ ⊢ (V, σ)֒→φ

˙
x̂.c := x, κ ⊢ (V, σ)֒→φ

κ ⊢ (M := N, σ) ֒→ φ

˙
κ ⊢ (V, σ[c 7→ V ])֒→φ

x̂.x; N, κ ⊢ (M, σ) ֒→ φ

κ ⊢ (N, σ) ֒→ φ

κ ⊢ (M ; N, σ) ֒→ φ

˙
x̂.x; N, κ ⊢ (V, σ)֒→φ

x̂.x N, κ ⊢ (M, σ) ֒→ φ
κ ⊢ (M N, σ) ֒→ φ

x̂.V x, κ ⊢ (N, σ) ֒→ φ
˙
x̂.x N, κ ⊢ (V, σ)֒→φ

˙
κ ⊢ (λx : τ.M, σ)֒→φ
κ ⊢ (λx : τ.M, σ) ֒→ φ

κ ⊢ (M ′ [V /y], σ) ֒→ φ

κ ⊢ (M [rec x : τ.M /x], σ) ֒→ φ

˙
x̂.(λy : τ.M ′ ) x, κ ⊢ (V, σ)֒→φ

κ ⊢ (rec x : τ.M , σ) ֒→ φ

Table XVII.

45

Object logic encoding of typing for PCF:= terms

∗
∗
∗
prog typeof
V (abs T R) (arr T U ))
λl( n(typeof n (T l) ⇒ htypeof (R l n) (U l)i) :: nil)
prog (typeof∗ (app∗ M N ) T )
(htypeof ∗ M (arr∗ U T )i∗ ::∗ htypeof ∗ N U i∗ ::∗ nil∗ )
∗
∗
prog (typeof
V (rec T R) T )
λl( n(typeof n (T l) ⇒ htypeof (R l n) (T l)i) :: nil)
prog (typeof∗ (ref∗ M ) (refty∗ T ))
(htypeof ∗ M T i∗ ::∗ nil∗ )
nil∗
prog (typeof∗ (deref∗ M ) T )
(htypeof ∗ M (refty∗ T )i∗ ::∗ nil∗ )
nil∗
prog (typeof∗ (assign∗ M N ) T )
(htypeof ∗ M (refty∗ T )i∗ ::∗ htypeof∗ N T i∗ ::∗ nil∗ )
prog (typeof∗ (sequence∗ M N ) T )
(htypeof ∗ M U i∗ ::∗ htypeof∗ N T i∗ ::∗ nil∗ )
nil∗

nil∗
nil∗
nil∗

nil∗

derivation of more than one Ci . In the specification of typing, no linear assumptions
are introduced, so LL will be empty. In general, we will use linear formulas (C1 ,
. . . , Cn ) in the bodies of specification clauses; we use intuitionistic formulas (B1 ,
. . . , Bn ) only where we specifically wish to preclude the use of linear assumptions.
This is only done in one clause in the encoding of the operational semantics, and
will be discussed when it is introduced. We extend the abbreviation convention
of Section 5.2 to the constants of this section. Thus (typeof∗ m t) abbreviates
(λl typeof (m l) (t l)), (refty∗ t) abbreviates (λl refty (t l)), etc.
The semantics for PCF:= is more complicated than those in the previous sections.
The constant ⇓ now has type itm → ist → ians → atm. The object logic atom
(m, s) ⇓ f represents the evaluation of the term m in the state s yielding the final
answer f . State is encoded using the constants null st: ist and extend st: ilc →
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

46

·

R. C. McDowell and D. A. Miller

Table XVIII.

Object logic encoding of natural semantics for PCF:= (part I)

prog ((M, S) ⇓∗ F )
nil∗
(hns mach 1∗ init∗ (eval∗ M ) S F i∗ ::∗ nil∗ )
prog (ns mach 1∗ K I (extend st∗ C V S) F )
((contains ∗ C V −◦∗ hns mach 1∗ K I S F i∗ ) ::∗ nil∗ )
prog (ns mach 1∗ K I null st∗ F )
(hns mach 2∗ K I F i∗ ::∗ nil∗ )
nil∗
prog (collect state∗ (extend st∗ C V S))
(hcontains ∗ C V i∗ ::∗ hcollect state∗ Si∗ ::∗ nil∗ )
prog (collect state∗ null st∗ )
nil∗
nil∗

nil∗

nil∗

itm → ist → ist ; null st represents the state with no locations, and (extend st c v s)
represents the state obtained by adding the location c containing value v to the
state s. A value and a state are combined into an answer using the constant
answer: itm → ist → ians ; variables representing new locations are bound using
new: (ilc → ians ) → ians . Our specification of evaluation will also use the predicates
ns mach 1
ns mach 2
contains
collect state

:
:
:
:

icntn → iinstr → ist → ians → atm
icntn → iinstr → ians → atm
ilc → itm → atm
ist → atm .

The object logic atom ns mach 1 k i s f corresponds to the two judgements of
Table XVI. Continuations are constructed using init: icntn to represent the initial
continuation and ≻: (itm → iinstr ) → icntn → icntn to extend a continuation.
Instructions, constructed from the constants
eval
return
eval arg
apply

:
:
:
:

itm
itm
itm
itm

→ iinstr
→ iinstr
→ itm → iinstr
→ itm → iinstr

new ref
lookup
eval rvalue
update

:
:
:
:

itm
itm
itm
itm

→ iinstr
→ iinstr
→ itm → iinstr
→ itm → iinstr ,

are used to indicate the current task in the evaluation of a term. The object logic
atom ns mach 2 k i f is a variation of ns mach 1 k i s f which does not contain
the state; instead the contents of each location is recorded using the object logic
predicate denoted by the constant contains. The evaluation of terms is specified
using this distributed representation of state; the state portion of the final answer
is constructed again using the predicate collect state. The specifications for all of
these predicates are represented by the F Oλ∆IN definition in Tables XVIII and
XIX.
This encoding differs slightly from the continuation semantics in Table XVI.
The object logic judgement nil∗ ; ll ✄ hns mach 2 k (return v) f i∗ corresponds to the
˙
judgement κ ⊢ (v ′ , σ)֒→φ,
where κ is the continuation encoded by k, v ′ is the value
encode by v, σ is the state encoded by the list ll of contains assumptions, and φ is
the answer encoded by f . However, the specification for ns mach 2∗ k (return∗ v) f
takes the first instruction from k and substitutes in the value v to obtain the new
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

Table XIX.

·

47

Object logic encoding of natural semantics for PCF:= (part II)

prog (ns mach 2∗ init∗ (return∗ V ) (answer∗ V S))
(hcollect state∗ Si∗ ::∗ nil∗ )
nil∗
prog (ns mach 2∗ (I ≻∗ K) (return∗ V ) F )
(hns mach 2∗ K (λl I l (V l)) F i∗ ::∗ nil∗ )
nil∗
prog (ns mach 2∗ K (eval∗ (cell∗ C)) F )
(hns mach 2∗ K (return∗ (cell∗ C)) F i∗ ::∗ nil∗ )

nil∗

prog (ns mach 2∗ K (eval∗ (ref∗ M )) F )
nil∗
(hns mach 2∗ ((λlλv new ref v) ≻∗ K) (eval∗ M ) F i∗ ::∗ nil∗ )
prog (nsV
mach 2∗ K (new ref∗ V ) (new∗ F ))
λl( c(contains c (V l) −◦ hns mach 2 (K l) (return (cell c)) (F l c)i) :: nil∗ )
nil∗
prog (ns mach 2∗ K (eval∗ (deref∗ M )) F )
(hns mach 2∗ ((λlλv lookup v) ≻∗ K) (eval∗ M ) F i∗ ::∗ nil∗ )
nil∗
prog (ns mach 2∗ K (lookup∗ (cell∗ C)) F )
(hcontains ∗ C V i∗ ::∗ (contains ∗ C V −◦∗ hns mach 2∗ K (return∗ V ) F i∗ ) ::∗ nil∗ )
nil∗
prog (ns mach 2∗ K (eval∗ (assign∗ M N )) F )
(hns mach 2∗ ((λlλv eval rvalue v (N l)) ≻∗ K) (eval∗ M ) F i∗ ::∗ nil∗ )
nil∗
prog (ns mach 2∗ K (eval rvalue∗ V N ) F )
nil∗
(hns mach 2∗ ((λlλv update (V l) v) ≻∗ K) (eval∗ N ) F i∗ ::∗ nil∗ )
∗
∗
∗
prog (ns mach 2 K (update (cell C) V ) F )
(hcontains ∗ C W i∗ ::∗ (contains∗ C V −◦∗ hns mach 2∗ K (return∗ V ) F i∗ ) ::∗ nil∗ )
nil∗
prog (ns mach 2∗ K (eval∗ (sequence∗ M N )) F )
(hns mach 2∗ ((λlλv eval (N l)) ≻∗ K) (eval∗ M ) F i∗ ::∗ nil∗ )

nil∗

prog (ns mach 2∗ K (eval∗ (app∗ M N )) F )
(hns mach 2∗ ((λlλv eval arg v (N l)) ≻∗ K) (eval∗ M ) F i∗ ::∗ nil∗ )
nil∗
prog (ns mach 2∗ K (eval arg∗ V N ) F )
nil∗
(hns mach 2∗ ((λlλv apply (V l) v) ≻∗ K) (eval∗ N ) F i∗ ::∗ nil∗ )
prog (ns mach 2∗ K (apply∗ (abs∗ T R) V ) F )
nil∗
(hns mach 2∗ K (eval∗ (λl R l (V l))) F i∗ ::∗ nil∗ )
prog (ns mach 2∗ K (eval∗ (abs∗ T R)) F )
nil∗
(hns mach 2∗ K (return∗ (abs∗ T R)) F i∗ ::∗ nil∗ )
prog (ns mach 2∗ K (eval∗ (rec∗ T R)) F )
(hns mach 2∗ K (eval∗ (λl R l (rec (T l) (R l)))) F i∗ ::∗ nil∗ )

nil∗

instruction. This new instruction then determines the next step in the evaluation.
On the other hand, the rules of Table XVI examine the return value and the first
term of the continuation to determine the next evaluation step. Other than this
small difference, the encoding mirrors the continuation semantics very closely.
The distributed encoding of state in Tables XVIII, and XIX makes vital use of linear implication. Since each assumption of the form contains∗ c v is a linear assumption, it can only be used once. This linearity is used, for example, in the clause for
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

48

·

R. C. McDowell and D. A. Miller

ns mach 2 with the instruction (update∗ (cell∗ c) v); the desired behavior is that the
contents of location c be replaced by the value v. This clause has two linear formulas
in its body, hcontains∗ c wi∗ and (contains∗ c v −◦∗ hns mach 2∗ k (return∗ v) f i∗ ).
Each contains assumption must be used exactly once in the derivation of these two
formulas. Since there is no clause for contains in the object logic theory, the first
formula must be derived by the initial rule, and so will use the one assumption
representing the contents of location c. The remainder of the state is then available
for the other formula, which adds a new assumption about the contents of c and
then continues the evaluation encoded in the continuation k. The linearity of the
contains assumptions is also used in the clause for ns mach 2 with the instruction
(return∗ v) and the continuation init∗ . This clause represents the situation where
the evaluation is complete and we wish to construct the final answer from the value
v and the state encoded in the assumptions. The clause has the single linear formula
hcollect state∗ si∗ as its body. Thus the derivation of this formula must use all of
the contains assumptions; this ensures that the constructed state includes all of the
locations represented in the assumptions. Dually, the clause for ⇓ in Table XVIII
has a single intuitionistic formula hns mach 1∗ init∗ (eval∗ m) s f i∗ as its body.
This clause represents the situation where we wish to evaluate the term m in the
state s. Since the formula in the body is intuitionistic, it must be derived from an
empty set of linear assumptions. Since there are no linear formulas in the body, this
means that (m, s) ⇓∗ f is only derivable from an empty set of linear assumptions,
i.e., the state is entirely represented in s.
We also introduce typing predicates for continuations, instructions, and answers:
typeofcntn : icntn → ity → atm
typeofinstr : iinstr → ity → atm .

typeofans : ians → ity → atm

The object-level specification for these predicates is represented in F Oλ∆IN by the
definition of Table XX. A continuation has type (arr∗ t u) if it expects a value of
type t in order to produce a value of type u. Instructions are typed in the same way
as the corresponding terms. The type of an answer is the same as the type of its
value component under some typing assumptions for any new memory locations.
These assumptions must be consistent with the values stored in those locations;
this consistency is expressed by the predicate well typed: ist → atm.
We now present the theorems we have derived in F Oλ∆IN about this object logic
encoding of PCF:= . We will refer to the collected clauses of Tables XVII, XVIII,
XIX and XX as the definition D(PCF:= ). To simplify the presentation of our
theorems, we introduce several F Oλ∆IN predicates:
store : atmlst∗ → o
store typing : atmlst∗ → o
store typeof : atmlst∗ → atmlst∗ → o .

≡atml : atm∗ → atm∗ → o
≡∗i : i∗ → i∗ → o

The store predicate indicates that a list of object logic atoms is a valid distributed
encoding of state, that is, its elements are of the form contains∗ c v. The predicate
store typing holds if its argument is a valid list of typing assumptions for locations.
The store typeof predicate holds for a store and store typing if every location in
the store is assigned a type by the store typing that agrees with a type of the value
stored in the location. Finally, ≡atml and ≡itml encode syntactic identity over
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

·

Reasoning with Higher-Order Abstract Syntax

Table XX.

49

Encoding of typing for PCF:= continuations, instructions, and answers

prog (typeof∗cntn init∗ (arr∗ T T ))
nil∗
nil∗
∗
∗
∗
prog (typeof
V cntn (I ≻ K) (arr T U ))
(λl
v(typeof v (T l) ⇒ htypeofinstr (I l v) (T ′ l)i) ::∗
htypeof ∗cntn K (arr∗ T ′ U )i∗ ::∗ nil∗ )
nil∗
prog (typeof∗instr (eval∗ M ) T )
(htypeof ∗ M T i∗ ::∗ nil∗ )
nil∗
prog (typeof∗instr (return∗ V ) T )
(htypeof ∗ V T i∗ ::∗ nil∗ )
nil∗
prog (typeof∗instr (eval arg∗ M N ) T )
(htypeof ∗ M (arr∗ U T )i∗ ::∗ htypeof∗ N U i∗ ::∗ nil∗ )
prog (typeof∗instr (apply∗ M N ) T )
(htypeof ∗ M (arr∗ U T )i∗ ::∗ htypeof∗ N U i∗ ::∗ nil∗ )
prog (typeof∗instr (new ref∗ M ) (refty∗ T ))
(htypeof ∗ M T i∗ ::∗ nil∗ )
nil∗
prog (typeof∗instr (lookup∗ M ) T )
(htypeof ∗ M (refty∗ T )i∗ ::∗ nil∗ )
nil∗
prog (typeof∗instr (eval rvalue∗ M N ) T )
(htypeof ∗ M (refty∗ T )i∗ ::∗ htypeof ∗ N T i∗ ::∗ nil∗ )
prog (typeof∗instr (update∗ M N ) T )
(htypeof ∗ M (refty∗ T )i∗ ::∗ htypeof ∗ N T i∗ ::∗ nil∗ )

nil∗
nil∗

nil∗
nil∗

prog (typeof∗ans (answer∗ V S) T )
nil∗
(htypeof ∗ V T i∗ ::∗ hwell typed∗ Si∗ ::∗ nil∗ )
∗
∗ F) T)
prog (typeof
(new
ans
V
λl ( c(typeof (cell c) (refty (U l)) ⇒ htypeofans (F l c) (T l)i) :: nil)

nil∗

prog (well typed∗ null st∗ )
nil∗
nil∗
prog (well typed∗ (extend st∗ C V S))
(htypeof ∗ (cell∗ C) (refty∗ T )i∗ ::∗ htypeof∗ V T i∗ ::∗ hwell typed∗ Si∗ ::∗ nil∗ )
nil∗

the types atm∗ and i∗ . The definition D(store) for these predicates is presented in
Table XXI. The following theorem states that we have derived the subject reduction
and unicity of typing properties for PCF:= in F Oλ∆IN . The F Oλ∆IN derivations
again closely follow the informal proofs of these properties. We expect that the
determinacy of semantics is also derivable, but have not yet shown this. We use
the following abbreviations from Section 5.2: D(lists) for
D(list ∗ (atm)) ∪ D(list ∗ (prp)) ∪ D(list ∗∗ (atm)) ∪ D(list ∗∗ (prp)) ,
and D(evars ) for
D(evars(atm)) ∪ D(evars(prp)) ∪ D(evars(atmlst)) ∪ D(evars(prplst)) .

Theorem 9.1. The following formulas are derivable in F Oλ∆IN from the definition that accumulates D(nat ), D(lists), D(evars), D(linear ), D(PCF:= ), and
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

50

·

R. C. McDowell and D. A. Miller

Table XXI.

Meta-logic predicates for PCF:= stores

△

store LL = list LL ∧ ∀a(element a LL ⊃
∃c∃v(a ≡atm∗ (contains∗ c v)))
△

store typing IL = list IL ∧
∀a(element a IL ⊃
∃c∃t(a ≡atm∗ (typeof ∗ (cell∗ c) (refty∗ t)))) ∧
∀c∀t1 ∀t2 (element (typeof∗ (cell∗ c) (refty∗ t1 )) IL ⊃
element (typeof∗ (cell∗ c) (refty∗ t2 )) IL ⊃
t1 ≡i∗ t2 )
△

store typeof LL IL = ∀c∀v(element (contains ∗ c v) LL ⊃
∃t(element (typeof ∗ (cell∗ c) (refty∗ t)) IL ∧
IL; nil∗ ✄ htypeof ∗ v ti∗ ))
△

A ≡atm∗ A = ⊤
△

X ≡i∗ X = ⊤

D(store):
Subject reduction:
∀m∀s∀f (✄(h(m, s) ⇓∗ f i∗ ) ⊃
∀ts∀t(store typing il ⊃ il; nil∗ ✄ hwell typed∗ si∗ ⊃
il; nil∗ ✄ htypeof∗ m ti∗ ⊃
il; nil∗ ✄ htypeof∗ans f ti∗ ))
∀ll∀k∀i∀f (store ll ⊃ nil∗ ; ll ✄ hns mach 2∗ k i f i∗ ⊃
∀il∀t∀u(store typing il ⊃ store typeof ll il ⊃
il; nil∗ ✄ htypeof∗cntn k (arr∗ t u)i∗ ⊃
il; nil∗ ✄ htypeof∗instr i ti∗ ⊃
il; nil∗ ✄ htypeof∗ans f ui∗ ))
Unicity of typing:
∀m∀t1 ∀t2 (✄htypeof∗ m t1 i∗ ⊃ ✄htypeof∗ m t2 i∗ ⊃ t1 ≡i∗ t2 )
Proof. The derivation of the unicity of typing is by complete induction on the
height of the first typing derivation ✄htypeof∗ m t1 i∗ . Let P1 be the predicate
λil∀a(element a il ⊃ ∃x∃t(a ≡atm∗ (typeof∗ (fst∗i x) t)))
and P2 the predicate
λil∀x∀t1 ∀t2 (element (typeof∗ x t1 ) il ⊃ element (typeof∗ x t2 ) il ⊃ t1 ≡i∗ t2 ) .
These predicates encode the requirements that the list of assumptions contains only
typing assignments for variables and assigns only one type to any one variable. Our
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

·

51

induction predicate IP is then
λj∀il(list il ⊃ P1 il ⊃ P2 il ⊃
∀m∀t1 ∀t2 (seqj il nil∗ htypeof∗ m t1 i∗ ⊃
il; nil∗ ✄ htypeof∗ m t2 i∗ ⊃ t1 ≡i∗ t2 )) .
The details of the proof are presented in McDowell [1997].
10. RELATED WORK
There are several approaches others have taken to reason about higher-order abstract syntax encodings directly in a formalized meta-language. Despeyroux, Felty,
and Hirschowitz in [1994; 1995] show that induction principles for a restricted form
of second-order abstract syntax can be derived in the Coq proof development system. To keep the definitions monotone, they introduce a separate type for variables
and explicit coercions from variables to other types. For example, their constructors
for λ-terms would be
var : vr → tm

abs : (vr → tm) → tm

app : tm → tm → tm ,

and the corresponding definition of typeof would be
typeofvr : vr → ty → o

typeof : tm → ty → o

△

typeof (var X) T = typeofvr X T
△
typeof (abs M ) (arr T U ) = ∀x(typeofvr x T ⊃ typeof (M x) U )
△
typeof (app M N ) T = ∃u(typeof M (arr u T ) ∧ typeof N u) .
This is similar to our use of the two predicates hyp and conc in our encoding of
intuitionistic logic in Section 4.2. Notice that the type tm does not occur negatively
in the type of any of its constructors, nor does the predicate typeof occur negatively
in its definition. This allows Coq to automatically construct induction principles
for tm and typeof. Since object-level variable binding is still represented by metalevel λ-abstraction, the object language still inherits α-equivalence from the metalanguage. Because the abstraction is over the type vr, however, meta-level βreduction cannot be used for substitution.1 These approaches also lessen the power
of the meta-level cut rule as a reasoning tool. Suppose that ∀x(typeofvr x T ⊃
typeof (M x) U ) and typeof N T are derivable. In contrast to our encoding, it is
not immediate that substituting N for (var x) in (M x) yields a term M ′ such that
typeof M ′ U is derivable. Thus of the three key benefits to higher-order abstract
syntax, they only retain α-conversion. In addition, the Coq type (vr → tm) includes
functions besides those expressible as λ-terms, so the type tm includes expressions
that do not encode terms of the object language. They avoid these exotic terms
1 Here

we are comparing the object system encodings. It is true that our explicit eigenvariable
encoding style requires an explicit definition of substitution for the specification logic. So at the
specification logic level of our framework, we too lose some of the benefits of higher-order abstract
syntax. However, at the level of the object system, we use a true higher-order abstract syntax
encoding with all of its benefits. Since we expect there to be only a few specification logics, but
many object systems, it seems worth putting the extra effort into the specification logic to reap
the benefit for the object systems.
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

52

·

R. C. McDowell and D. A. Miller

through the definition and use of a validation predicate. The term language of
F Oλ∆IN , unlike that of Coq, does not include primitive recursion, so these exotic
terms do not arise in our framework.
Despeyroux, Pfenning, and Schürmann [1997] address the problem of exotic terms
by using a modal operator to distinguish the types of parametric functions (expressible as λ-terms) from the types of arbitrary functions. As a result, their calculus
allows primitive recursive functionals while preserving the adequacy of higher-order
abstract syntax encodings. This represents a start toward a logical framework supporting meta-theoretic reasoning, higher-order abstract syntax, and the judgmentsas-types principle. In such a framework a derivation would be represented as a
function whose type is the derived property. Thus the → type constructor must
be rich enough to include the mappings from derivations to derivations such as the
realizations of case analysis and induction. Their work is orthogonal to our work
presented in this paper. We are not attempting to support the judgments-as-types
principle, so the types of our meta-logic are only used to encode syntactic structure.
Thus we can restrict these types to include only λ-terms, ensuring the adequacy of
encodings in higher-order abstract syntax. They, on the other hand, do not address
the issue of induction principles for higher-order abstract syntax, or more generally,
the issue of formal reasoning about higher-order abstract syntax encodings.
Schürmann and Pfenning [1998] construct a meta-logic M2 to reason about deductive systems represented in LF. Their approach is similar in spirit to ours in
that there are three levels: the deductive system(s) under consideration, the logic
in which the deductive systems are encoded, and the logic in which meta-theoretic
analysis takes place. The meta-logic M2 includes a case-analysis rule comparable
to our defL rule and a recursion rule that generalizes our natL rule. Their intermediate logic, LF, includes dependent types, and so is richer than the intermediate
logics we consider. On the other hand, our meta-logic is a general framework capable of supporting a variety of intermediate logics (such as intuitutionistic and linear
logics), whereas M2 is designed for the specific, fixed intermediate logic LF.
Still another strategy for meta-theoretic reasoning about higher-order abstract
syntax encodings is to perform each case of a proof in the meta-logic, but verify the
completeness of the proof outside the logical framework. Rohwedder and Pfenning
[1992; 1996] investigate the design and implementation of such external validity
conditions.
Matthews seeks to reconcile the advantages of LF-style encodings with the facilities for meta-theoretic analysis found in theories of inductive definitions [Matthews
1997]. His approach has some similarity to our own, in that he creates a three-level
hierarchy, with each level being encoded in the previous. As in our approach, his
top level contains a definition facility and induction principles for reasoning about
encodings at the next level. However, his logic at the intermediate level contains
only an implication connective and no quantifiers. Thus he does not address the
treatment of object-level bound variables, a major feature of higher-order abstract
syntax and, consequently, of our work.
11. CONCLUSION
In this paper we have presented a single and simply motivated meta-logic F Oλ∆IN .
We used this meta-logic as the basis of a framework for formal reasoning about
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

·

53

systems expressed in higher-order abstract syntax, avoiding the apparent tradeoff
between the benefits of this representation technique and the ability to perform
meta-theoretic analyses of encodings. We demonstrated this framework on encodings of three programming languages encompassing both functional and imperative
paradigms. A number of significant theorems about these languages were derived
in this framework, including unicity of typing and subject reduction. The flexibility of the framework was also shown through the use of intuitionistic and linear
specification logics.
The meta-logic F Oλ∆IN has also been used to reason about simulation and bisimulation in abstract transition systems and CCS [McDowell et al. ]. These transition
systems did not contain binding operators, and so both the specification and reasoning was done in the meta-logic. We have already begun using the techniques
presented in the current paper to extend that work to the setting of applicative
bisimulation [Abramsky 1990]. It would also be interesting to use Howe’s technique
[Howe 1996] to prove the congruence of bisimulation in our framework.
Additional work in analysis of programming languages along the lines of Part III
could also be done. Time precluded us from proving the determinacy of evaluation for PCF:= , for example, and a transition semantics for the language could be
constructed and shown to be equivalent to the natural semantics we constructed.
It would also be interesting to formalize other analyses; Hannan and Miller [1992],
for example, construct abstract machines from operational semantics by applying
a series of transformations and argue informally that the transformations preserve
correctness. Richer languages could also be considered, including features such as
concurrency, exceptions, and polymorphism. Linear logic has been used to specify
such features in a manner that is suitable for use in our setting [Chirimar 1995;
Miller 1996].
The formal derivations described in this paper have been checked using the Pi
derivation editor of Lars-Henrik Eriksson [Eriksson 1994]; see McDowell [1997] for
a discussion of the effectiveness of this editor for constructing F Oλ∆IN proofs. An
important next step in this line of work is to implement a theorem prover that
provides semi-automated assistance in proving F Oλ∆IN theorems. Miller and Wajs
are building a prototype theorem prover named Iris [Wajs 2000] within λProlog.
Finally, alternatives to the explicit eigenvariable encoding of Section 4.4 could
be explored. Although this encoding supports the higher-order abstract syntax
representation of bound variables and allows substantial meta-theoretic analysis, it
does have some drawbacks. The pervasive presence of the evs parameter representing the free variable list is somewhat cumbersome, and numerous lemmas must be
proved to show that various properties are preserved by extensions of this list or
substitution for free variables. The obvious alternative, a de Bruin-style encoding
of free variables, would require a similar amount of work and would not support the
higher-order abstract syntax representation for bound variables. It is important to
point out that this issue relates to the encoding of the specification logic, not the
object systems, of our framework. Thus these lemmas need to be proved only once
for any specification logic, not for every object system, and so the representational
advantage of higher-order abstract syntax for the object systems is preserved.
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

54

·

R. C. McDowell and D. A. Miller

ACKNOWLEDGMENTS

We would like to thank Frank Pfenning for helpful feedback on early drafts of this
work and Lars-Henrik Eriksson for making his Pi derivation editor [Eriksson 1994]
available to help check the formal derivations described here. Two anonymous
referees provided extensive comments that helped improve the presentation of this
paper.
REFERENCES
Abramsky, S. 1990. The lazy lambda calculus. In Research Topics in Functional Programming,
D. Turner, Ed. Addison Wesley, 65–117.
Avron, A., Honsell, F., Mason, I. A., and Pollack, R. 1992. Using typed lambda calculus
to implement formal systems on a machine. Journal of Automated Reasoning 9, 309–354.
Basin, D. A. and Constable, R. L. 1993. Metalogical frameworks. In Logical Environments,
G. Huet and G. D. Plotkin, Eds. Cambridge University Press, 1–29.
Cervesato, I. and Pfenning, F. 1996. A linear logic framework. In Proceedings, Eleventh Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, New Brunswick,
New Jersey, 264–275. An extended version of this paper will appear in Information and Computation.
Chirimar, J. 1995. Proof theoretic approach to specification languages. Ph.D. thesis, University
of Pennsylvania.
Church, A. 1940. A formulation of the simple theory of types. Journal of Symbolic Logic 5,
56–68.
Despeyroux, J., Felty, A., and Hirschowitz, A. 1995. Higher-order abstract syntax in Coq.
In Second International Conference on Typed Lambda Calculi and Applications, M. DezaniCiancaglini and G. Plotkin, Eds. Lecture Notes in Computer Science, vol. 902. Springer-Verlag,
124–138.
Despeyroux, J. and Hirschowitz, A. 1994. Higher-order abstract syntax with induction in
Coq. In Proceedings of the Fifth International Conference on Logic Programming and Automated Reasoning, F. Pfenning, Ed. Lecture Notes in Artificial Intelligence, vol. 822. SpringerVerlag, 159–173.
Despeyroux, J., Pfenning, F., and Schürmann, C. 1997. Primitive recursion for higher-order
abstract syntax. In Third International Conference on Typed Lambda Calculi and Applications,
R. Hindley, Ed.
Eriksson, L.-H. 1991. A finitary version of the calculus of partial inductive definitions. In
Proceedings of the Second International Workshop on Extensions to Logic Programming, L.-H.
Eriksson, L. Hallnäs, and P. Schroeder-Heister, Eds. Lecture Notes in Artificial Intelligence,
vol. 596. Springer-Verlag, 89–134.
Eriksson, L.-H. 1993. Finitary partial inductive definitions as a general logic. In Proceedings
of the Fourth International Workshop on Extensions to Logic Programming. Lecture Notes in
Artificial Intelligence, vol. 798. Springer-Verlag, 94–119.
Eriksson, L.-H. 1994. Pi: an interactive derivation editor for the calculus of partial inductive
definitions. In Proceedings of the Twelfth International Conference on Automated Deduction,
A. Bundy, Ed. Lecture Notes in Artificial Intelligence, vol. 814. Springer-Verlag, 821–825.
Felty, A. 1993. Implementing tactics and tacticals in a higher-order logic programming language. Journal of Automated Reasoning 11, 1 (August), 43–81.
Felty, A. and Miller, D. 1988. Specifying theorem provers in a higher-order logic programming language. In Ninth International Conference on Automated Deduction, E. Lusk and
R. Overbeck, Eds. Springer-Verlag, 61–80.
Girard, J.-Y. 1992. A fixpoint theorem in linear logic. A message posted on the mailing
list linear@cs.stanford.edu, see http://www.csl.sri.com/linear/mailing-list-traffic/
www/07/mail_3.html.
Gunter, C. A. 1992. Semantics of Programming Languages: Structures and Techniques. Foundations of Computing. MIT Press.
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

Reasoning with Higher-Order Abstract Syntax

·

55

Hallnäs, L. 1991. Partial inductive definitions. Theor. Comput. Sci. 87, 115–142.
Hannan, J. and Miller, D. 1992. From operational semantics to abstract machines. Math.
Struct. Comput. Sci. 2, 4, 415–459.
Hannan, J. J. 1990. Investigating a proof-theoretic meta-language for functional programs.
Ph.D. thesis, University of Pennsylvania.
Harper, R., Honsell, F., and Plotkin, G. 1993. A framework for defining logics. Journal of
the ACM 40, 1, 143–184.
Hodas, J. and Miller, D. 1994. Logic programming in a fragment of intuitionistic linear logic.
Information and Computation 110, 2, 327–365.
Howe, D. J. 1996. Proving congruence of bisimulation in functional programming languages.
Information and Computation 124, 2, 103–112.
Huet, G. 1975. A unification algorithm for typed λ-calculus. Theor. Comput. Sci. 1, 27–57.
Magnusson, L. and Nordström, B. 1994. The ALF proof editor and its proof engine. In
Types for Proofs and Programs, H. Barendregt and T. Nipkow, Eds. Number 806 in Lecture
Notes in Computer Science. Springer-Verlag, 213–237.
Matthews, S. 1997. A practical implementation of simple consequence relations using inductive
definitions. In Proceedings of the 14th Conference on Automated Deduction, W. McCune, Ed.
Springer-Verlag.
Matthews, S., Smaill, A., and Basin, D. 1993. Experience with FS0 as a framework theory.
In Logical Environments, G. Huet and G. Plotkin, Eds. Cambridge University Press, 61–82.
McDowell, R. 1997. Reasoning in a logic with definitions and induction. Ph.D. thesis,
University of Pennsylvania.
McDowell, R. and Miller, D. 2000. Cut elimination for a logic with definitions and induction.
Theor. Comput. Sci. 232, 91–119.
McDowell, R., Miller, D., and Palamidessi, C. Encoding transition systems in sequent calculus. To appear in Theoretical Computer Science. Preliminary version appeared as [McDowell
et al. 1996].
McDowell, R., Miller, D., and Palamidessi, C. 1996. Encoding transition systems in sequent
calculus: Preliminary report. In Proceedings of the 1996 Workshop on Linear Logic. Electronic
Notes in Theoretical Computer Science, vol. 3. Elsevier.
Miller, D. 1990. Abstractions in logic programs. In Logic and Computer Science, P. Odifreddi,
Ed. Academic Press, 329–359.
Miller, D. 1991. A logic programming language with lambda-abstraction, function variables,
and simple unification. J. Logic and Comput. 1, 4, 497–536.
Miller, D. 1996. Forum: A multiple-conclusion specification language. Theor. Comput.
Sci. 165, 201–232.
Miller, D. and Nadathur, G. 1987. A logic programming approach to manipulating formulas
and programs. In IEEE Symposium on Logic Programming, S. Haridi, Ed. 379–388.
Miller, D., Nadathur, G., Pfenning, F., and Scedrov, A. 1991. Uniform proofs as a
foundation for logic programming. Annals of Pure and Applied Logic 51, 125–157.
Mitchell, J. C. 1995. Foundations for Programming Languages. MIT Press.
Paulson, L. C. 1986. Natural deduction as higher-order resolution. J. Logic Program. 3,
237–258.
Pfenning, F. 1989. Elf: A language for logic definition and verified metaprogramming. In
Proceedings,Fourth Annual Symposium on Logic in Computer Science. IEEE Computer Society
Press, 313–321.
Pfenning, F. 1995. Structural cut elimination. In Proceedings, Tenth Annual IEEE Symposium
on Logic in Computer Science, D. Kozen, Ed. IEEE Computer Society Press, 156–166.
Pfenning, F. and Elliot, C. 1988. Higher-order abstract syntax. In Proceedings of the ACMSIGPLAN Conference on Programming Language Design and Implementation. 199–208.
Pfenning, F. and Rohwedder, E. 1992. Implementing the meta-theory of deductive systems.
In Proceedings of the Eleventh International Conference on Automated Deduction, D. Kapur,
Ed. Lecture Notes in Artificial Intelligence, vol. 607. Springer-Verlag, 537–551.
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

56

·

R. C. McDowell and D. A. Miller

Rohwedder, E. and Pfenning, F. 1996. Mode and termination analysis for higher-order logic
programs. In Proceedings of the European Symposium on Programming. 296–310.
Schroeder-Heister, P. 1992. Cut-elimination in logics with definitional reflection. In Nonclassical Logics and Information Processing, D. Pearce and H. Wansing, Eds. Lecture Notes in
Computer Science, vol. 619. Springer-Verlag, 146–171.
Schroeder-Heister, P. 1993. Rules of definitional reflection. In Proceedings, Eighth Annual
IEEE Symposium on Logic in Computer Science, M. Vardi, Ed. IEEE Computer Society Press,
222–232.
Schürmann, C. and Pfenning, F. 1998. Automated theorem proving in a simple meta logic for
LF. In Proceedings of the 15th International Conference on Automated Deduction (CADE-15),
C. Kirchner and H. Kirchner, Eds. Lecture Notes in Computer Science, vol. 1421. SpringerVerlag, 286–300.
Scott, D. S. 1969. A type theoretical alternative to CUCH, ISWIM, OWHY. Unpublished
manuscript.
VanInwegen, M. 1996. The machine-assisted proof of programming language properties. Ph.D.
thesis, University of Pennsylvania.
Wajs, J. D. 2000. Design and implementation of a theorem prover for operational semantics.
M.S. thesis, Pennsylvania State University.
Received Month Year; revised Month Year; accepted Month Year.

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD.

