Research Themes and Contributions

I provide a summary of my primary research themes and contributions. These are listed in roughly chronological order. When I do not explicitly use the first person pronoun, I summarize work done with several colleagues. Follow links to find references to the others involved.

My research has focused on applying proof theory concepts to various computer science problems. When I have developed such applications in the areas of computing and reasoning, I have often been forced to develop new features in proof theory to treat suitably the demands of such applications.

**Expansion proofs:**
In my 1983 Ph.D. thesis, I defined a generalization of Herbrand disjunctions
for higher-order classical logic. That generalization, called
*expansion trees* and *expansion proofs*, provides a
generalization of Herbrand's theorem for higher-order logic as well as
a parallel proof structure for classical logic.

**Unification:** I have worked on the following aspects of the
unification of simply typed λ-terms (aka higher-order
unification). • The soundness of skolemization (used to
simplify quantifier alternation) within higher-order
logic. • The treatment of unification under a mixed prefix (i.e.,
without skolemization). • The design and analysis of a subset of
higher-order unification, now called *higher-order pattern
unification*, that appears to be the weakest extension of
first-order unification that respects α, β, and
η-conversions.

**Logic programming:**
Starting about 1985, I worked with several students and colleagues
on a decade-long effort to use proof theory as a foundation for logic
programming languages. The following resulted from that work.
(See also my 2021 paper *A Survey
of the Proof-Theoretic Foundations of Logic Programming*.)

A view of logic programming as

*proof-search*and the use of*uniform proofs*to describe both goal-directed search and backchaining. This work provided an early example of a comprehensive*focused proof system*.A formal treatment of higher-order quantification (at predicate and non-predicate types) in logic programming.

The description of logic programming within (higher-order) intuitionistic logic that allowed logic programming to embrace such abstraction mechanisms as modules, abstract datatypes, bound variables, and higher-order programming.

The design of the λProlog programming language. This language, designed jointly with Nadathur, has had several implementations since its inception in 1985. Two recent implementations are Teyjus and ELPI.

The design of two linear logic programming languages. Lolli extended λProlog by adding linear implication while Forum extended Lolli by adding the multiplicative disjunction and multiplicative false. These linear logic programming languages greatly extended the expressiveness of Prolog and λProlog.

**λ-tree syntax:** λProlog was the first programming
language to provide a data structure with language support for
bindings modulo α-conversion and substitution.
The
term *higher-order
abstract syntax*
is often used for describing this approach to syntactic representation
in λProlog.
Unfortunately, that term has grown to encapsulate the modeling of
bindings as functions within functional programs, an approach that
yields a limited and semantically
questionable approach to abstract syntax. As a result, I introduced the
term *λ-tree syntax* to denote the
specific treatment of bindings available in systems such as
λProlog, Isabelle/Pure, and Twelf.
A key feature of λ-tree syntax is the need to support
the *mobility of binders*:
bound variables are never replaced by
free variables but rather by other bound variables.
An extensive set of examples
using λ-tree syntax in specifications and programs is
available.

**Linear logic as a logical framework:** Working with Nigan and
Pimentel, we showed that linear logic can
specify
several proof systems for classical, intuitionistic,
and linear logics. Such specifications come with easily checked
necessary conditions for determining if the specified proof systems
satisfy cut elimination. This framework has been extended with
subexponentials
and has
been implemented.

**Operational semantics:** I have often turned to the specification
of operational semantics as a domain to apply logic
programming and relational specifications. In particular,
λ-tree syntax can make such specifications straightforward
and elegant, and both small-step and big-step specifications lend
themselves immediately to logic programming specifications. Linear
logic can also be used to great effect in the specification of
big-step operational semantics. I have written
an overview
article on this topic.

**Proof theory for fixed points:** Logic programming, at least as
developed above, is limited to essentially *reachability*. One
can go beyond such judgments if one embraces forms of induction.
Since induction is generally used to encode properties of first-order
term structures, Baelde and I have studied the proof theory of the triple
consisting of first-order quantification, first-order equality, and
induction and co-induction. The resulting proof theory has allowed
establishing a logical duality between finite success and finite failure
and a proof-theoretic treatment of simulation and bisimulation.
This work provided the basis of the model checking system
Bedwyr. I have
also argued that the proof theory
of MALL (multiplicative-additive linear logic) extended with fixed
points provides a basis for model checking.

**∇-quantification:** When extending the proof theory for
fixed points and first-order quantification to capture
λ-tree syntax, Tiu and I introduced
the ∇-quantifier to denote
generic quantification: the presence of negation-as-failure
forces a separation of generic from universal quantification. Such
an extension has made it possible to directly perform model checking
on π-calculus expressions. The ∇-quantifier is built into
the Abella theorem prover and
the Bedwyr model
checker.

**Formalized meta-theory:** One reason to design and use logic
programming languages based on rich logical principles is to
support broad avenues for formally reasoning about what they
specify. The first tool that does such formalized reasoning about
λProlog is the Abella
theorem prover. This system employs a *two-level logic*
approach to specifications and reasoning. Some of the most elegant
formal treatments of meta-theory for the λ-calculus and
π-calculus can be found in
the Abella
repository.

** Focused proof systems:** From our work in the 1980s, it
was clear that the sequent calculus, as defined by Gentzen, was too
chaotic to apply directly to many computer science and proof
theory problems. Some of our early work used

** Foundational proof certificates:**
Focused proofs are organized into two phases. One phase
involves the application of invertible inference rules. The second
phase involves making a series of (possibly non-invertible) inference
rules. This latter
phase involves making the choices that eventually lead to a final proof.
The structure of focused proofs allows them to be used as protocols
between a proof checker and a proof certificate. Based on this notion
of protocol, my ERC Advanced Grant
ProofCert
has funded the development of
the foundational
proof certificate approach to defining the proof semantics of a
wide range of proof evidence for classical and intuitionistic
logics.