Saarland University Computer Science


Introduction to Computational Logic Gert Smolka

Resources

Lecture Notes

Coq

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.
  • 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.
  • Per Martin-Löf, Intuitionistic Type Theory.
    Bibliopolis, 1984.
  • Biographies of important logicians