To learn about logical languages and specifications, to understand the logical basis of functional programming und the principles of computability. Connection between algorithms and proofs.

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.

ECTS breakdown

24 h: 12 lectures a 2 h

16 h: solving 2 sheets of ex. a 7 ex.

4 h: typing solutions in LaTeX

30 h: preparation for final examination

1 h: final examination

-----------------------------------------

75 h = 3 ECTS