Lambda Calculus as formalism for Computations and Proofs

Credits	8 credit points
Instructors	Barendregt, H.P. (Radboud Universiteit Nijmegen), Wiedijk, F. (Radboud Universiteit Nijmegen)
E-mail	henk@cs.ru.nl, freek@cs.ru.nl
Aim	Understanding lambda calculus - as formalism to capture computations; - as formalism to capture proofs; - as mathematical objects to be studied for their intrinsic structure.
Description	Untyped lambda calculus 06.2 Lambda calculus 13.2 Computability 20.2 Meta-theory 27.2 Boehm Trees Typed lambda calculus 05.3 Simply typed lambda calculus 12.3 Higher order lambda calculus 19.3 Pure type systems 26.3 Inductive types Typed lambda calculus for mathematics 02.4 Constructive proof checking 16.4 Classical proof checking 23.4 De Bruijn criterion Advanced topics in lambda calculus 07.5 Strong Normalization 14.5 Statman Hierarchy 21.5 Inconsistencies
Organization	Mondays 14:00-16:45. Lecture-Exercises-Lecture
Examination	Part of the intention of the course is to learn to 'write mathematics'. Exam date resit: June 25, 2012. 13.30-16.30 h in BBL 007, Utrecht
Literature	Textbook: The lambda calculus, its syntax and semantics. (H. Barendregt, 1984) Will be used in the course. Some chapters of "Lambda calculi with types" (H. Barendregt, W. Dekkers, R. Statman) will also be used. As the first book is perhaps no longer available and the second one perhaps not yet, a reader may be made.
Prerequisites	Some logic is a pro: predicate logic; computability theory.

Last changed: 22-05-2013 16:30