DPL
Description	This dissertation introduces denotational proof languages (DPLs). DPLs can be used to express and check (validate) formal proofs. DPL proofs are typically readable, writable, compact, and easy to check. Syntactically, DPL proofs are generated by context-free grammars in such a way that the text of the proof reflects its logical structure. Semantically, the formal meaning of a DPL proof is specified relative to a given assumption base, which is a set of premises, i.e., a set of propositions that we take for granted for the purposes of the proof. The key idea is that if a DPL proof is sound, then its meaning (denotation) is the conclusion established by the proof; if the proof is unsound, then its meaning is error. To obtain that meaning, we evaluate the proof in accordance with the formal semantics of the language. Evaluation will either produce the advertised conclusion, which will verify that the proof is sound, or else it will generate an error, which will indicate that the proof is unsound. Thus in DPLs evaluation is tantamount to proof checking. We illustrate the core ideas by introducing CN D, a simple DPL for classical firstorder logic with equality. We develop the theory of CN D in detail, prove its soundness and completeness, present dozens of sample proofs, and develop a number of proof optimization procedures that remove redundancies and unnecessary "detours". We also discuss CN D as a formal analysis of the concept of deduction, and compare it with previous formalizations such as Hilbert calculi, sequent systems, and proof trees. We then introduce the *u-calculus, a terse formal system that can be viewed as a unifying framework for DPLs, much as the *-calculus can be seen as a unifying formal framework for functional programming languages. The *u-calculus allows for proof abstraction via methods. Methods are to proofs what procedures are to computations. They are essential for task decomposition and complexity management in proof engineering. Methods are made possible by a careful integration of computation and deduction: the *u-calculus can be used both for programming and for proofs. More interestingly, we show how methods, when combined with recursion, pattern matching, etc., can be used for proof search and theorem proving. We work out the rudiments of the theory and metatheory of the *u-calculus, and present several examples of *u systems.
Deliverables	Athena, dissertation
Contributions	DPL proofs are typically readable, writable, compact, and easy to check.
Researchers	Kostas Arkoudas
Language	ML
Subprojects	subprojects