Introduction to Computational Logic: 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,
Proofchecking using Dependent Type Systems.
Handbook of Automated Reasoning, Volume II, 11491240.
Elsevier 2001.

JeanYves Girard,
Proofs and Types.
Cambridge University Press, 1990.

Dag Prawitz,
Natural Deduction, a Prooftheoretical 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,
FirstOrder 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
Last Change: Thu 01 Jan 1970 00:00:00 UTC