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