syntax of Lambda-calculus, combinatory logic, Lambda-conversion, reduction, normal form, confluence, termination, beta-reduction, eta-reduction, the Church-Rosser theorem, Lambda-theories, Lambda-definability, number systems, recursive functions, undecidability. Typed Lambda-Calculus, Curry-Howard isomorphism.