Denotational Proof Languages
             --------------------------------

In this talk I will describe a new approach to the subject of
machine-checkable formal proofs. Most previous work on mechanized 
formal proofs has focused on type theories and the Curry-Howard 
isomorphism, where a proof D is represented by a lambda-calculus 
term M and the conclusion of D is represented by the type of M, 
in such a way that D is sound iff M is well-typed. Under that 
correspondence (also known as the "proofs-as-programs correspondence"), 
proof checking is reduced to type checking. Unfortunately, even 
simple logics require sophisticated dependent-type systems that 
are in general undecidable, and so a large amount of type information 
must be explicitly inserted in the proofs in order to keep 
type checking decidable. This results in large proofs that are 
difficult to read and write. 
We propose denotational proof languages (DPLs) as a new alternative.
In a DPL, the syntax of the proofs reflects the structure of
the underlying logic. The meaning (denotation) of a proof is
identified with the conclusion that the proof purports to establish,
and is formally specified by the semantics of the language based
on the abstraction of assumption bases. In this scheme, evaluation
amounts to proof checking: if a proof is sound, then evaluation will 
produce the relevant conclusion; if the proof is unsound, then evaluation
will result in an error. This denotational view also paves the way
for a formal theory of proof equivalence, making it possible to answer
questions such as "Exactly when should two proofs be considered 
equal?", "When is one proof more efficient than another?", "What
kinds of optimizations can be performed on proofs, and when is it
safe to perform such optimizations?", and so on. In this talk I 
will discuss the main ideas behind DPLs and their potential applications
to software engineering, using a toy DPL as a concrete example.