Proof Theory Foundations
Intuitionistic proofs correspond to functional programs and vice versa. Since the celebrated discovery of this Curry-Howard isomorphism, similar relationships have guided our understanding of advanced programming language constructs, for example, for distributed computation or staged computation. Every computer scientist should therefore understand the basic structure of proofs and their computational interpretation.
In this course we explore the theory of proofs, emphasizing the fundamental principles that underly systems of logical inference. A student taking this course will learn
- how to define and justify logical systems from first principles
- how to assess the intrinsic coherence of a logic
- how to uncover the computational meaning of proofs
- how to construct effective systems of proof search
The course is divided into four lectures.
- Natural Deduction: how to define logics
- Verifications: the intrinisic meaning of propositions
- Sequent Calculus: searching for proofs
- Focusing: from myopic to prescient inference
Below are some basic references. Most
closely related to the material in lectures 1-3 (although not in the
same order) are
Lecture 1: Judgments and Propositions, Lecture 2: Proofs as Programs and Lecture 8: Sequent Calculus from a course
on Modal Logic at Carnegie Mellon in Spring 2010. Attached below are lectures notes for Lecture 4: Focusing.
Untersuchungen über das logische Schließen.
Mathematische Zeitschrift, 39:176-210, 405-431, 1935.
English translation in M. E. Szabo, editor, The Collected Papers
of Gerhard Gentzen, pages 68-131, North-Holland, 1969.
Basic historical reference; introduces both the natural deduction
and the sequent calculus.
Almquist & Wiksell, Stockholm, 1965.
Investigates the metatheory of natural deduction.
W. A. Howard.
The formulae-as-types notion of construction.
In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry:
Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479-490.
Academic Press, 1980.
Hitherto unpublished note of 1969, rearranged, corrected, and
annotated by Howard.
The note introducing the Curry-Howard isomorphism for natural
deduction. Curry had previously described it for combinatory
On the meanings of the logical constants and the justifications of
the logical laws.
Technical report, Scuola di Specializzazione in Logica Matematica,
Dipartimento di Matematica, Università di Siena, April 1983.
Reprinted in the Nordic Journal of Philosophical Logic 1(1),
pp. 11-60, 1996.
Lays out the justification of the definition of the logical connectives
by distinguishing judgments from propositions.
The Logical Basis of Metaphysics.
Harvard University Press, Cambridge, Massachusetts, 1991.
The William James Lectures, 1976.
Analysis of verificationists and pragmatist points of view and their harmony.
Frank Pfenning and André Platzer.
Notes for a course at Carnegie Mellon University, Spring 2010.
Lectures 1, 2, 8.
Lectures notes closely related to lectures 1-3 presented at the summer
Frank Pfenning and Rowan Davies.
A judgmental reconstruction of modal logic.
Mathematical Structures in Computer Science, 11:511-540, 2001.
Notes to an invited talk at the Workshop on Intuitionistic Modal
Logics and Applications (IMLA'99), Trento, Italy, July 1999.
Introduces explicit notions of local soundness and completeness
and applies them in the richer setting of modal logic where additional
Structural cut elimination I. Intuitionistic and classical logic.
Information and Computation, 157(1/2):84-141, March 2000.
Introduces the cut elimination proof of lecture 3 and its
formalization in a logical framework.
Logic programming with focusing proofs in linear logic.
Journal of Logic and Computation, 2(3):197-347, 1992.
The seminal paper on focusing, treating classical linear logic.
Chuck Liang and Dale Miller.
Focusing and polarization in linear, intuitionistic, and classical
Theoretical Computer Science, 410(46):4747-4768, November
A paper that also treats polarization and intuitionistic logic.
Probably the closest reference for Lecture 4.
Sean McLaughlin and Frank Pfenning.
Efficient intuitionistic theorem proving with the polarized inverse
In R.A.Schmidt, editor, Proceedings of the 22nd International
Conference on Automated Deduction (CADE-22), pages 230-244, Montreal,
Canada, August 2009. Springer LNCS 5663.
An application of focusing in a realistic theorem prover.
The Logical Basis of Evaluation Order and Pattern-Matching.
PhD thesis, Department of Computer Science, Carnegie Mellon
University, May 2009.
Available as Technical Report CMU-CS-09-122.
An application of focusing in the design of programming languages.