Introduction to Computational Logic: Resources

Programming Systems

Teaching

Main page

Timetable

Resources

Registration

Services

Exams and Grade

Login

Discussion Board

Lecture Notes

• Lecture notes (appear as the lectures proceed)


• Library LFS (html overview) (code, compile with coqc)
• Library PropL (html overview) (code, compile with coqc)
• Library PfTerms (html overview) (code, compile with coqc)
• Library Semc (html overview) (code, compile with coqc)
• Library Semi (html overview) (code, compile with coqc)
• Library LFS2 (html overview) (code, compile with coqc)
• Library Deci (html overview) (code, compile with coqc)


• Lecture notes from last year (Summer 2012)

Coq

• Coq Home Page (download system here, we are using version 8.4)
• 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.
• 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 Clipala)

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.
• 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.
• Melvin Fitting,
  First-Order Logic and Automated Theorem Proving. 2nd edition.
  Springer, 1996.
• Herbert B. Enderton,
  A Mathematical Introduction to Logic. 2nd edition.
  Academic Press, 2001.
• Peter B. Andrews,
  An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof.
  Kluwer Academic Publishers, 2002.
• Patrick Blackburn, Maarten de Rijke and Yde Venema,
  Modal Logic.
  Cambridge University Press, 2001.
• 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.
• Henk Barendregt, Wil Dekkers, Richard Statman,
  Lambda Calculus with Types.
  Cambridge University Press, 2013.
• Biographies of important logicians