Semantics: Resources
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
Coq.
Lecture Notes
There are rudimentary
and some Coq developments
complementing the primary texts.
Coq code used in lectures:
Main Texts
Coq
Further Reading

Gert Smolka and Chad Brown,
Lecture notes of the course Introduction to Computational Logic

Robert Harper,
Practical Foundations for Programming Languages

Adam Chlipala,
Certified programming with dependent types using Coq

Glynn Winskel,
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, ChungKil Hur, Andrew Kennedy, and Conor McBride,
Strongly Typed Term Representations in Coq.
Journal of Automated Reasoning, March 2011.
Contains simply typed lambda calculus with typeindexed syntax.

Zhaohui Luo,
Computation and Reasoning: A Type Theory for Computer Science.
Oxford University Press, 1994.
Last Change: Mon Oct 16 13:11:03 2017