Denotational Proof Languages

What are DPLs?

DPLs (Denotational Proof Languages) are languages for expressing formal proofs and proof-search

algorithms in arbitrary logics. Roughly speaking, there are two types of DPLs: type-alpha and type-omega.

Type-a DPLs allow for proof presentation and checking, but not for proof search. Type-w DPLs are

supersets of type-a DPLs, so they allow for proof presentation and checking, but they also allow for

proof search, and indeed for arbitrary computation. So type-w DPLs are actually Turing-complete

programming languages, as well as proof frameworks (like ACL2 or HOL, but with important

differences). The languages are structured in such a way that soundness is ensured: the conclusion

of any proof D is guaranteed to be a logical consequence of the assumption base in which D was

evaluated (more on assumption bases below).

There are two main innovations behind DPLs, the first of a syntactic and the second of a semantic kind.

On the syntactic front, DPLs have formalized key notions such as assumption scope and eigenvariable

scope in novel ways (most notably, without reducing them to variable scope in the typed lambda calculus,

as is done in Curry-Howard systems via higher-order abstract syntax); and based on those formalizations,

syntax forms such as assume, pick-any, and pick-witness have been introduced that closely capture the

most common and useful idioms of mathematical reasoning. In addition, type-w DPLs have introduced

a notion of teasing apart the syntax of computation and deduction in a way that allows the two to be integrated

seamlessly and soundly. Semantically, the main contribution of DPLs is the introduction of assumption bases.

The introduction of assumption bases as a fundamental semantic abstraction on a par with lexical environments,

stores, and continuations allows for an elegant treatment of proof theory, even for logics that have been difficult

to formalize in a non-graphical manner, such as Fitch-style natural deduction. The approach is quite distinct from

that of systems based on higher-order constructive type theory, such as LF, Coq, or Nuprl. It is more similar to

systems of the LCF variety (HOL, Isabelle, etc.), but again, the introduction of assumption bases and the

syntactic separation of deduction and computation bring several advantages, e.g. sequents are no longer necessary,

and proofs can be written in a style that is much closer to the natural deduction format used in practice. Even a static

type system is not necessary in a type-w DPL (by contrast, a strong static type system is perhaps the

hallmark of LCF-style systems; it is absolutely essential for them in order to ensure soundness). In addition,

assumption-base semantics enable a rich theory of observational equivalence for proofs, greatly facilitating

the formulation---and answering---of questions such as the following:

· When are two proofs equivalent?

· When can one proof D₁ be safely substituted for another proof D₂ inside a third proof D?

· When is one proof more “efficient” than another?

For instance, using the theory of assumption-base observational proof equivalence, we have developed

a procedure for simplifying natural-deduction proofs that often results in dramatic size reductions.

The DPL style of presentation has been applied to numerous logics, including zero-, first-, and higher-order

natural deduction for classical logic, intuitionist logic, modal and temporal logics, Hoare-Floyd program logics,

and others. Here are some papers on DPLs:

• An introduction to DPLs
• Type-omega DPLs
• DPL dissertation

Athena

Athena is a type-w DPL for polymorphic multi-sorted first-order natural deduction – in the Fitch style, not based on sequents.

It includes a higher-order functional language in the tradition of Scheme. It was developed by Konstantine Arkoudas at MIT in

1998. It has been used to develop and check proofs in several applications, A tutorial will be coming soon, but in the meanwhile

here are a few other resources that can get someone up and going in using the language:

• A very brief note on how to declare a logic vocabulary (function and predicate symbols, etc.) and how to build propositions

in Athena.

• A fairly complete but terse description of the syntax and evaluation semantics of Athena.
• A list of Athena’s primitive methods and their semantics.
• Some problem sets from a DPL seminar that I ran at MIT a few years ago:

1. Problem set 1, and the solutions.
2. Problem set 2, and the solutions.
3. Problem set 3, and the solutions.
4. Problem set 4 (no solutions for this one).

• A recent paper using Athena: Integrating model checking and theorem proving for relational reasoning.

(The code for that project can be found here.)

More Athena resources (including distributions, Emacs environments, etc.).

David Musser was using Athena this last term (Fall 2003) for his course in Generic Programming,

and has put together a page with some Athena resources, including a couple of turorials with heuristics

on how to build Athena proofs, an Emacs environment for Athena. Athena distributions for Windows,

Linux, Solaris, and the Mac can also be found there.

Soon, those distributions will be found on this page, along with a forthcoming Athena tutorial and

a few other documents.