Formal Methods Foundation

Resources

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.

Softwares

• Coq: an interative proof assistant
• F#: Microsoft's next-generation functional language
• TeX & LaTeX: a scientific document preparing system. It's also helpful to use this package to typeset proof and this one to typeset code.