This course contains basic techniques and results of the theory of sequential functions as described by the lambda-calculus and combibatoru logic. The course contains the typed and untyped version of the formalism, as well as basic results concerning models of lambda-calulus. Lambda-calculus is important for understanding recursive constructs used in programming as well in the corresponding semantics constructs, and it provides a reference formalism useful for variaous applications.

Syllabus

Pure lambda-calculus: lambda-terms, structure of terms, equational theories.
Reductions: one-way transformations, general reductions, beta-reduction.
Lambda-calculus and computations: coding, recursive definitions, lambda-computability, fixed-point combinators, undecidable properties.
Modification of the theory: combinatory logic, extensionality, eta-reduction.
Typed lambda-calculus: types and terms, normal forms, set models, strong normalization, types as formulae.
Domain models: complete partial orders, domains, least fixed points, partiality.
Domain construction: compound domains, recursive domain construction, limit domains.

Literature

ZLATUŠKA, Jiří. Lambda-kalkul. Vyd. 1. Brno: Masarykova univerzita, 1993. 264 s. ISBN 80-210-0826-1. info
BARENDREGT, H. P. Lambda calculus : its syntax and semantics. Rev. ed. Amsterdam: Elsevier, 1998. xv, 621 s. ISBN 0-444-86748-1. info
HINDLEY, J. Roger and Jonathan P. SELDIN. Introduction to combinators and the lambda-calculus. Cambridge: Cambridge University Press, 1986. 359 s. ISBN 0-521-31839-4. info
AMADIO, Roberto M. and Pierre-Louis CURIEN. Domains and lambda-calculi. Cambridge: Cambridge University Press, 1998. xvi, 484 s. ISBN 0-521-62277-8. info

Assessment methods (in Czech)