Proof Theory Foundations
Intuitionistic proofs correspond to functional programs and vice versa. Since the celebrated discovery of this CurryHoward 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 13 (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.

Gerhard Gentzen.
Untersuchungen über das logische Schließen.
Mathematische Zeitschrift, 39:176210, 405431, 1935.
English translation in M. E. Szabo, editor, The Collected Papers
of Gerhard Gentzen, pages 68131, NorthHolland, 1969.
Basic historical reference; introduces both the natural deduction
and the sequent calculus.

Dag Prawitz.
Natural Deduction.
Almquist & Wiksell, Stockholm, 1965.
Investigates the metatheory of natural deduction.

W. A. Howard.
The formulaeastypes 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 479490.
Academic Press, 1980.
Hitherto unpublished note of 1969, rearranged, corrected, and
annotated by Howard.
The note introducing the CurryHoward isomorphism for natural
deduction. Curry had previously described it for combinatory
logic.

Per MartinLöf.
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. 1160, 1996.
Available electronically
Lays out the justification of the definition of the logical connectives
by distinguishing judgments from propositions.

Michael Dummett.
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.
Modal logic.
Notes for a course at Carnegie Mellon University, Spring 2010.
Lectures 1, 2, 8.
[Available electronically]
Lectures notes closely related to lectures 13 presented at the summer
school.

Frank Pfenning and Rowan Davies.
A judgmental reconstruction of modal logic.
Mathematical Structures in Computer Science, 11:511540, 2001.
Notes to an invited talk at the Workshop on Intuitionistic Modal
Logics and Applications (IMLA'99), Trento, Italy, July 1999.
[PDF]
Introduces explicit notions of local soundness and completeness
and applies them in the richer setting of modal logic where additional
judgments arise.

Frank Pfenning.
Structural cut elimination I. Intuitionistic and classical logic.
Information and Computation, 157(1/2):84141, March 2000.
[PDF]
Introduces the cut elimination proof of lecture 3 and its
formalization in a logical framework.

JeanMarc Andreoli.
Logic programming with focusing proofs in linear logic.
Journal of Logic and Computation, 2(3):197347, 1992.
The seminal paper on focusing, treating classical linear logic.

Chuck Liang and Dale Miller.
Focusing and polarization in linear, intuitionistic, and classical
logics.
Theoretical Computer Science, 410(46):47474768, November
2009.
[PDF]
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
method.
In R.A.Schmidt, editor, Proceedings of the 22nd International
Conference on Automated Deduction (CADE22), pages 230244, Montreal,
Canada, August 2009. Springer LNCS 5663.
[PDF]
An application of focusing in a realistic theorem prover.

Noam Zeilberger.
The Logical Basis of Evaluation Order and PatternMatching.
PhD thesis, Department of Computer Science, Carnegie Mellon
University, May 2009.
Available as Technical Report CMUCS09122.
An application of focusing in the design of programming languages.

Ċ ď Frank Pfenning, Jun 23, 2010, 6:56 AM
