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:

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:

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


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.