Semantics : Resources
Lecture Notes
 Lecture notes (appear as the lectures proceed)
last modified at:
February 03 2014
 Accompanying Coq developments (HTML movies powered by Proviola).
Coq
Literature

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

Xavier Leroy
Mechanized
semantics, with applications to program proof and compiler verification

Tobias Nipkow, Gerwin Klein
Concrete Semantics

Zhaohui Luo,
Computation and Reasoning: A Type Theory for Computer Science.
Oxford University Press, 1994.

JeanYves Girard,
Proofs and Types.
Cambridge University Press, 1990.

J. Roger Hindley and Jonathan P. Seldin,
Lambda Calculus and Combinators: An Introduction.
Cambridge University Press, 2008.

Henk Barendregt
The Lambda Calculus, Its Syntax and Semantics
NorthHolland Publishing Company, 1981

Henk Barendregt, Wil Dekkers, Richard Statman,
Lambda Calculus with Types.
Cambridge University Press, 2013.

Henk Barendregt and Herman Geuvers,
Proofchecking using Dependent Type Systems.
Handbook of Automated Reasoning, Volume II, 11491240.
Elsevier 2001.

Robert Harper,
Practical Foundations for Programming Languages

Per MartinLöf,
An Intuitionistic Theory of Types, original version from 1972.
Appears in Giovanni Sambin and Jan Smith (editors),
TwentyFive Years of Constructive Type Theory,
Proceedings of a Congress Held in Venice, October 1995;
Clarendon Press, Oxford, 1998.

Per MartinLöf,
Intuitionistic Type Theory,
Volume1 of Studies in Proof Theory, Bibliopolis, 1984.

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.
Slides