|
Link to the Homepage: Introduction to Computational Logic
| |
Biographies of important logicians | |
Andrews, Peter B. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof Kluwer Academic Publishers 2002 | |
Baader, Franz and Nipkow, Tobias Term Rewriting and All That Cambridge University Press 1999 | |
Bertot, Yves and Casteran, Pierre Interactive Theorem Proving and Program Development Springer 2004 | |
Forster, Thomas Logic, Induction and Sets Cambridge Univ. Press 2003 | |
Girard, Jean-Yves Proof and Types Cambridge University Press 1993 | |
Hindley, James Roger and Seldin Jonathan P. Lambda-Calculus and Combinators Cambridge University Press 2008 | |
![]() |
Institute for Advanced Study Homotopy type theory Princeton, NJ 2013 |
Luo, Zhaohui Computation and Reasoning: A Type Theory for Computer Science Oxford University Press 2002 | |
![]() |
Per, Martin-Löf Intuitionistic Type Theory Bibliopolis 1984 |
Prawitz, Dag Natural deduction - A proof-theoretical study Dover Publications 2006 | |
Robinson, Alan Handbook of Automated Reasoning - Band 2 Course Relevant Article: Proof Assistants using Dependent Type Systems (p. 1149-1238) by Barendregt, Henk and Geuvers, Herman North Holland 2001 | |
Sørensen, Morten Heine and Urzyczyn, Pawel Lectures on the curry-howard isomorphism Elsevier 2006 | |
Troelstra, Anne Sjerp and Schwichtenberg, Helmut Basic proof theory Cambridge University Press 2003 |