We will mainly follow the ebook
Software Foundations by Benjamin Pierce and others.
We will also rely on the textbook
Types and Programming Languages,
again written by Benjamin Pierce.
Throughout the course we will use the proof assistant
There are rudimentary
and some Coq developments
complementing the primary texts.
Coq code used in lectures:
Gert Smolka and Chad Brown,
Lecture notes of the course Introduction to Computational Logic
Practical Foundations for Programming Languages
Certified programming with dependent types using Coq
The Formal Semantics of Programming Languages: An Introduction.
MIT Press, 1993.
Franz Baader and Tobias Nipkow,
Term Rewriting and All That.
Cambridge University Press, 1998.
Nick Benton, Chung-Kil Hur, Andrew Kennedy, and Conor McBride,
Strongly Typed Term Representations in Coq.
Journal of Automated Reasoning, March 2011.
Contains simply typed lambda calculus with type-indexed syntax.
Computation and Reasoning: A Type Theory for Computer Science.
Oxford University Press, 1994.
Last Change: Sat Aug 17 14:14:48 2019