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). In addition, type-omega 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. One of the main contribution of DPLs is the introduction of assumption-base semantics.

An assumption base is just a set of premises: a set of propositions
that we take for granted for the purposes of a given stretch of
logical discourse. This is traditionally known in logic as a
"context," a notion that has been around for a while, particularly
in connection with sequent systems, where the basic unit of inference
is a pair consisting of a context and a conclusion. What is
novel about DPLs is how assumption bases are used to give formal
semantics to proofs: the idea that * the formal
meaning of a proof is a function over assumption bases *.
That is, the meaning of a proof is specified relative to
a given assumption base, in the same way
that in denotational semantics the formal meaning of an imperative
program is a function over stores. Unlike sequent systems,
where the manipulation of the context is explicit and falls on the user,
the manipulation and threading of the context in DPLs is
implicit and relegated to the underlying semantics---again, much as the manipulation
and threading of the store in imperative languages is hidden from
the user.

This turns out to be an apt viewpoint that is particularly conducive to giving a rigorous semantics to Fitch-style natural deduction. In general, 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. The approach is different 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 proof abstraction is facilitated.

Moreover, assumption-base semantics enable a rich theory of observational equivalence for proofs, facilitating the formulation---and answering---of questions such as the following:

- When are two proofs equivalent?
- When can one proof be safely substituted in place of another proof inside a third proof?
- When is one proof more efficient than another?

- The
dissertation
that introduced DPLs.

- A
paper
that introduces a type-alpha DPL.

- A
paper
that introduces a type-omega DPL. You can also download some software that
implements the language introduced in the paper. You can
do this by getting the
ndlOmega.zip
or
ndlOmega.tar file,
depending on whether you are using Windows or Unix. Once you have
downloaded the sources, consult the file README on how to get the
system up and running. You will need to have
SML-NJ installed,
including ML-Lex, ML-Yacc, and the compilation manager (CM).
Any version higher than 110.29 should work.
If you have any questions or problems, please
email
Konstantine Arkoudas :
konstantine "at" alum.mit.edu.

- NDL:
This is an example of a type-alpha DPL. It's implemented in Java.

- Athena:
This is an example of a type-omega DPL. It's implemented in SML.