Material
-
Introduction to Lambda Calculus
Henk Barendregt and Erik Barendsen
lecture notes, revised edition, December 1998, March 2000
(local pdf,
local pdf)
-
Introduction to Type Theory
Herman Geuvers
Language Engineering and Rigorous Software Development (Revised Tutorial
Lectures), LNCS 5520, pp. 1 – 56, 2008
doi:
10.1007/978-3-642-03153-3_1
(local pdf)
-
Proof Assistants using Dependent Type Systems
Henk Barendregt and Herman Geuvers
chapter 18 of the Handbook of Automated Reasoning, pp. 1149 – 1238,
Elsevier Science Publishers, 2001
doi:
10.1016/b978-044450813-3/50020-5
(local pdf)
-
Logic Verification
Femke van Raamsdonk
course notes, Vrije Universiteit Amsterdam, Autumn 2008
(local pdf)
-
Parallel Reductions in λ-Calculus
Masako Takahashi
Information and Computation 118(1), pp. 120 – 127, 1995
doi:
10.1006/inco.1995.1057
(local pdf)
-
Coq in a Hurry
Yves Bertot
3rd cycle, Types Summer School, 2010
(local pdf)
Background Material