Textbooks and Reference

There are no required textbooks for this course, for no single book will cover the contents of this course in sufficient depth and width. Instead, we'll follow the lecture notes handed out in class closely. For those who are anxious for this, here are some books for reference:

• Software Foundations. Benjamin Pierce, &c. Book Draft.
• Certified Programming with Dependent Types. Adam Chlipala. Book Draft.
• Types and Programming Languages. Benjamin Pierce. MIT Press. 2002.
• Constructive Logic. Frank Pfenning. Book Drafts.
• A Mathematical Introduction to Logic, Second Edition. Herbert B. Enderton. Academic Press. 2000.
• Lectures on the Curry-Howard Isomorphism. Morten Heine B. Sorensen and Pawel Urzyczyn. Book Drafts.
• Logic in Computer Science: Modelling and Reasoning about Systems 2nd Edition. Michael Huth and Mark Ryan. Cambridge University press. 2004.
• The Calculus of Computation. Decision Procedures with Applications to Verification. Aaron R. Bradley; Zohar Manna. Springer. 2007.
• Decision Procedures: An Algorithmic Point of View 2nd ed. Daniel Kroening, Ofer Strichman. Springer. 2016.

Software

• Coq: an interactive proof assistant
• Z3: an open source SMT solver from Microsoft research
• TeX & LaTeX: a scientific document preparing system. It's also helpful to use this package to typeset proof and this one to typeset code.