Obsah

- Introduction to Lambda Calculus, Barendregt & Barensen, 2002.
- Section 1 - all.
- Section 2 - up to Def. 2.14; you don't need to remember the rest - the operations on Church numerals, just their basic definition is enough.
- Section 3 - just Definitions 3.1 and 3.2, Theorem 3.17
- Section 4 - up to 4.12. (no need to know the proof of Church-Roser theorem), and 4.20-4.23.

- Converting λ terms into the combinatory calculi: Combinatory calculi, in particular section
*Completeness of the S-K basis*. (A bit more advanced article I wrote on this topic can be found in The Monad Reader, Issue 17:*The Reader Monad and Abstraction Elimination*.)

- Natural deduction - you can skip all parts concerning quantifiers as we're interested only in propositional logic.

- Lectures on the Curry-Howard Isomorphism. M.H. Sørensen, and P. Urzyczyn. Elsevier, 2006.
**Type theory and lambda calculus, System F**- Proofs and Types. Girard J-Y, Lafont Y, and Taylor P. Cambridge Press, 1989.

**Data structures**- Purely Functional Data Structures. Chris Okasaki. Cambridge University Press, 1993. PDF

**Category theory**- Category Theory - Lecture Notes for ESSLLI. Michael Barr, and Charles Wells. PDF.

**Dependent types**- Programming in Martin-Löf's Type Theory. Bengt Nordström, Kent Petersson and Jan M. Smith. Oxford University, 1990.
- Dependently Typed Programming in Agda. Ulf Norell. 2009.
- Certified Programming with Dependent Types. Adam Chlipala.
- Software Foundations. Benjamin C. Pierce, Chris Casinghino, Michael Greenberg, Vilhelm Sjöberg, Brent Yorgey.

Church defined δ-reduction as follows:

Term is in δ-normal form if:

- doesn't contain any subterm of the form (λx.M)N
- doesn't contain any subterm of the form δMN, where M aand N are combinators (have no free variables).

We define δ-reduction as:

- δMN →
_{δ}T (true) if both M and N are in δ-normal form, don't contain variables, and they are α-equal. - δMN →
_{δ}F (false) if both M and N are in δ-normal form, don't contain variables, and they are not α-equal.

(Literature: http://bit.ly/rwdhf0, which is according to http://books.google.com/books?id=KCOuGztKVgcC.)