Introduction to Computational Logic

• We follow the MPCTT book (under construction, may be updated)
• Coq files accompanying the chapters of the book (at github, may be updated)
• Videos including lectures
• We use the Coq Proof assistant: 
  • Coq Homepage
  • Reference Manual
  • Standard Library
  • Commands
  • Tactics
• Related online books
  • An online book on software foundations starting with an introduction to Coq (by Benjamin Pierce and others)
  • A book on certified programming with dependent types using Coq (by Adam Chlipala)
  • Computational type theory, a survey by Robert L. Constable in Scholarpedia
  • The HoTT book, online book on (homotopy) type theory

 

Installing the Coq proof assistant

Make sure you have the Coq proof assistant working in the first week, best before the first lecture.  Directions for installation are at the Coq site.  Beginners are encouraged to use one of the binary installers (MacOs, Windows, Linux) and the accompanying CoqIDE.  You can get help with the installation in the office hours and the tutorials.

 

Literature

• Zhaohui Luo,
  Computation and Reasoning: A Type Theory for Computer Science.
  Oxford University Press, 1994.
• Henk Barendregt and Herman Geuvers,
  Proof-checking using Dependent Type Systems.
  Handbook of Automated Reasoning, Volume II, 1149--1240.
  Elsevier 2001.
• Jean-Yves Girard,
  Proofs and Types. 
  Cambridge University Press, 1990.
• Dag Prawitz,
  Natural Deduction, a Proof-theoretical Study.
  Dover Publications, 2006. (first published 1965)
• The Univalent Foundations Program
  Homotopy Type Theory.
  Institute for Advanced Study, Princeton, 2013.
• M.H. Sorensen and P. Urzyczyn,
  Lectures on the Curry-Howard Isomorphism.
  Elsevier, 2006.
• Yves Bertot and Pierre Castéran,
  Interactive Theorem Proving and Program Development.
  Coq'Art: The Calculus of Inductive Constructions.
  Springer, 2004.
• Thomas Forster,
  Logic, Induction and Sets.
  Cambridge University Press, 2003.
• Peter B. Andrews,
  An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof.
  Kluwer Academic Publishers, 2002.
• J. Roger Hindley and Jonathan P. Seldin,
  Lambda Calculus and Combinators: An Introduction.
  Cambridge University Press, 2008.
• Anne S. Troelstra and Helmut Schwichtenberg,
  Basic Proof Theory. 2nd edition.
  Cambridge University Press, 2000.
• Franz Baader and Tobias Nipkow,
  Term Rewriting and All That.
  Cambridge University Press, 1998.
• Per Martin-Löf, Intuitionistic Type Theory.
  Bibliopolis, 1984.
• Biographies of important logicians