Introduction to Computational Logic Gert Smolka

Lecture Notes

• This years lecture notes:
  • First three chapters from 2014 lecture notes
    (D-04-20, D-04-25, D-04-27, D-05-02, D-05-04)
  • Induction and Recursion for Numbers (D-05-09)
  • Proof Irrelevance and Elim Restriction (D-05-11)
  • Inductive Predicates (D-05-16, D-05-18, D-05-23)
  • Lists (D-05-30)
  • Decidability (D-06-01, D-06-06)  
  • Option Types and Sigma Types  (D-06-13, D-06-20)
  • Constructive Choice (D-06-22)
  • Retracts (D-06-27, D-06-29, D-07-04, D-07-06)
  • Natural Deduction (D-07-11, D-07-13, D-07-18)
  • Classical Tableau Method
  • Identity Proofs 
• Videos explaining how to write proofs (by hand and in Coq)
• Assignments
• Lecture note from 2014 

Coq

• Coq Home Page (download system here, we are using version 8.6)
• There are two user interfaces for Coq: CoqIDE and Proof General. You can choose which one you want to use.
  • CoqIDE: You can download and install CoqIDE along with the rest of Coq from the Coq Home Page. Documentation about CoqIDE can be found here.
  • Proof General: Proof General is an emacs mode that supports many theorem provers, including Coq. You can download Proof General from this link. Using Proof General, Company Coq is an extension allowing you to look up lemmas and the Coq Documentation.
• Coq Documentation
• 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)

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