Functional programming and lambda calculus: Syntax of lambda expressions and their evaluation. Function applications and currying. Lambda abstractions. Operational semantics of lambda calculus: bound and free variables, betaconversion, alphaconversion, interconvertibility. Rewriting systems, termination, confluence, ChurchRosser property, normal forms. Connection to the pure lambda calculus and related problems. Representation of boolean formulas, natural numbers, tuples. Computable functions: total recursive, partial recursive. Fixed point theorems, undecidable properties. Recursive functions, Y combinator as a lambda abstraction. Denotational semantics of lambda calculus. Translation of higher order functional languages into lambda calculus: letexpressions, letrecexpressions, hierarchical data types, and pattern matching. Functional programming and ordered algebras: Specification of abstract data types: heterogeneous (manysorted) algebras, their subalgebras, morphisms, and products; principle of the finitary algebraic recursion; equational theories, manysorted equational logic; equational specification; initial semantics and operational semantics. Ordered algebras, their morphisms and products. Varieties of ordered algebras and their characterization of free ordered algebras. Inequational logic. Strict ordered algebras, omegaordered algebras. Recursive programming schemes and their semantics, computed values, symbolic solutions, semantic equivalence. Stack model of evaluation of symbolic expressions: Functional programs as sequences of symbolic expressions. Stack model of evaluation. Semantic language elements: primitive procedures, definable procedures, special forms (operators), macros, environments, pairs. Extensions of the evaluation process: lexical and dynamic scoping, lazy evaluation, cached evaluation, imperative features in programming, escaping functions, current continuations, indeterminism, and parallelism. Interpreters and compilers of functional programming languages and their implementation methods.


Barendregt H. P. (1997). The Lambda Calculus: its Syntax and Semantics. 2nd reprint. Elsevier, Amsterdam.

Bird R., Wadler P. (1988). Introduction to Functional Programming. Prentice Hall, Englewood Cliffs, New Jersey.

H. Abelson, G. J. Sussman. (1985). Structure and Interpretation of Computer Programs (SICP). MIT Press.

Church A. (1941). The Calculi of Lambda Conversion. Princeton University Press, Princeton, NJ.

Leeuwen, J. van (ed.). (1994). Handbook Of Theoretical Computer Science: Formal Models and Semantics. Volume B, Elsevier.

Manis V. S., Little J. J. (1995). The Schematics of Computation. Prentice Hall, Englewood Cliffs, New Jersey.

Peyton Jones S. L. (1987). The Implementation of Functional Programming Languages. Prentice Hall.

Wechler W. (1992). Universal Algebra for Computer Scientists. SpringerVerlag Berlin Heidelberg.

Zlatuška J. (1993). Lambdakalkul. Vydavatelství MU, Brno.
