Overview
Logic provides computer science with both a unifying foundational framework and a tool for modeling. In fact, logic has been called "the calculus of computer science". It not only plays a crucial role in diverse areas such as artificial intelligence, computational complexity, distributed computing, database systems, hardware design, but it is also closely connected to programming languages.
This course gives an introduction to proof theory and highlights the deep connection between logic on the one hand and computation and programming languages on the other hand. We concentrate on the natural deduction system and the Curry-Howard somorphism. In particular, we concentrate on the relationship of propositions and types and proofs and programs. Some of the topics we will cover: intuitionistic logic, lambda-calculus, Curry Howard isomorphism, sequent calculus, consistency, (strong) normalization, first-order logic, induction.
A draft of the course notes covering the material is available here. These are course notes which have been used in the graduate course "Comp527: Logic and Computation" at McGill University and adopt material developed by Frank Pfenning (Carnegie Mellon University).
Supplementary Reading
The following books provide excellent introductions to part of this material:
- Jean-Yves Girard, "Proofs and Types". Cambridge University Press, 1989.
- Dag Prawitz. Natural Deduction. Almquist & Wiksell, Stockholm, 1965.
If you want to read more about some of the topics, we discuss in class, you can take a look at some of the research papers below:
- 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.
Original paper where the natural deduction and sequent calculus was introduced.
- 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.
Lays out the justification of the definition of the logical connectives by distinguishing judgments from propositions.
- 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 introduces the Curry-Howard isomorphism for natural deduction.
- Frank Pfenning. Structural cut elimination I. Intuitionistic and classical logic. Information and Computation, 157(1/2):84-141, March 2000.
Introduces the cut elimination proof of described in the lecture and its formalization in a logical framework.
- 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 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.
- Rowan Davies and Frank Pfenning. A modal analysis of staged computation. Journal of the ACM, 48(3):555-604, May 2001. Shows how modal logic can serve as a foundation for partial evaluation and staged computation.
- Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. Transactions on Computational Logic, 9(3), 2008. Generalizes the previous work on judgmental reconstruction of modal logic.
- Andrew Cave, Francisco Ferreira, Prakash Panangaden, and Brigitte Pientka. Fair reactive programming, POPL'14. Defines a constructive version of linear temporal logic together with fixpoints as a basis for programming reactive systems.
- 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.
- Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747-4768, November 2009. [PDF]
The paper describes polarization and intuitionistic logic.
- Hugo Herbelin. A lambda-calculus structure isomporphic to the Gentzen-style Sequent Calculus Structure. Selected Papers from the 8th International Workshop on Computer Science Logic (CSL'94), pages 61-75, Springer, 1995.
The paper introduces a proof term calculus for the sequent calculus which is based on spines, i.e. list of arguments). This new calculus is isomorphic to the structure of Gentzen-style sequent calculus.
- Pierre-Louis Curien and Hugo Herbelin. The duality of computation, 5th ACM SIGPLAN International Conference on Functional Programming (ICFP'00), ACM 2000.
The first paper to justify the relevance of sequent calculus to the computational study of the lambda-calculus.
- 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.
- Neelakantan R. Krishnaswami. Focusing on Pattern Matching, 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'09), pages 366-378, ACM.
Copyright
Instructor generated course materials (e.g., handouts, notes, summaries, homeworks, exam questions, etc.) are protected by law and may not be copied or distributed in any form or in any medium without explicit permission of the instructor. Note that infringements of copyright can be subject to follow up by the University under the Code of Student Conduct and Disciplinary Procedures.