Frank Pfenning

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.

  1. Natural Deduction: how to define logics
  2. Verifications: the intrinisic meaning of propositions
  3. Sequent Calculus: searching for proofs
  4. 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.

  1. Gerhard Gentzen. 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.

  2. Dag Prawitz. Natural Deduction. Almquist &amp Wiksell, Stockholm, 1965.

    Investigates the metatheory of natural deduction.

  3. 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 logic.

  4. Per Martin-Lö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. 11-60, 1996. Available electronically

    Lays out the justification of the definition of the logical connectives by distinguishing judgments from propositions.

  5. 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.

  6. 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 1-3 presented at the summer school.

  7. 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. [PDF]

    Introduces explicit notions of local soundness and completeness and applies them in the richer setting of modal logic where additional judgments arise.

  8. Frank Pfenning. Structural cut elimination I. Intuitionistic and classical logic. Information and Computation, 157(1/2):84-141, March 2000. [PDF]

    Introduces the cut elimination proof of lecture 3 and its formalization in a logical framework.

  9. Jean-Marc Andreoli. 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.

  10. Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747-4768, November 2009. [PDF]

    A paper that also treats polarization and intuitionistic logic. Probably the closest reference for Lecture 4.

  11. 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 (CADE-22), pages 230-244, Montreal, Canada, August 2009. Springer LNCS 5663. [PDF]

    An application of focusing in a realistic theorem prover.

  12. Noam Zeilberger. 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.

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