README.md

Class Notes and Materials for Maynooth University CS424, Fall 2015

http://github.com/barak/mu-cs424-f2015

• Instructor: Prof Barak A. Pearlmutter
• Office: Computer Science, Ugly New Building room 132
• Class: Tue 09:00 CB1; Thu 14:00 CB1
• Office Hours: TBA

Administrative Matters

• Scribes for notes.
• Scheme/Prolog/Haskell syntax highlighting or Markdown format.
• In git, on GitHub.
• Feel free to help with notes (fix typos as you read), send pull requests, etc.

Reference Materials

λ-Calculus Reference Materials

• Peter Selinger's Lecture notes on the lambda calculus, http://arxiv.org/abs/0804.3434

• Blelloch and Harper, λ-Calculus: The Other Turing Machine, manuscript: https://www.cs.cmu.edu/~rwh/papers/lctotm/cs50.pdf slides: https://www.cs.cmu.edu/~rwh/talks/cs50talk.pdf

• http://www-verimag.imag.fr/~iosif/LogicAutomata07/lambda-calculus-slides.pdf (Nice slide deck, I used it in class)

• A Tutorial Introduction to the Lambda Calculus, by Raúl Rojas, http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf (9 pages of summary, with some problems for the reader.)

• Introduction to Lambda Calculus, by Henk Barendregt and Erik Barendsen, http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf (53 pages, rather technical treatment includes proofs and diagrams, includes the Typed λ-Calculus.)

• A short introduction to the Lambda Calculus, by Achim Jung http://www.cs.bham.ac.uk/~axj/pub/papers/lambda-calculus.pdf (10 very readable pages, with historic context and intuitions and exercises.)

• Lambda-calculus: Types and Models, by Jean-Louis Krivine, translated from French by René Cori, http://www.pps.univ-paris-diderot.fr/~krivine/articles/Lambda.pdf (Full-length 206-page book, and an excellent one too! Ends by formulating and proving Gödel's Theorem in λ-Calculus instead of the usual Turing Machine formulation.)