Syllabus
Introduction to lambda calculus, functional programming and the Haskell programming language. Operational semantics of functional programs, beta-reduction and normal forms of expressions (NF, HNF, WHNF).
Functions as first-class objects of functional languages. Recursive functions, higher-order functions, combinators.
Church encoding of data types. Algebraic data structures. Pattern matching.
Typed lambda calculi. Intuitionistic logic, natural deduction calculus and its connection to typed lambda calculi. Curry-Howard correspondence. Basic notions of combinatory logic. Dependent types.
Expression type inference. Hindley/Milner type system and principal type inference algorithm. Generating expressions of given type and its applications.
Ad-hoc polymorphism - type classes. Connection to logic programming.
Recursive, infinite, inductive and coinductive data structures. Total functional programming. Type systems describing provably total functions - Gödel System T and Girard-Reynold System F.
Basic notions from category theory in the context of functional languages. Functors, Kleisli category, monads.
Facultative topics:
Type systems for working with side effects. Monads, unique types, linear types and linear logic.
Extension of standard type systems used in various functional languages. Type systems in imperative languages. Generalized algebraic data structures.
Functional reactive programming (FRP).
Web page: http://tomkren.cz/fp/, older web page: http://petr.pudlak.name/fp/.
Annotation
Basic notions, data structures and techniques in functional programming, focused on its theoretical foundations.
Oriented mainly towards functional programming language Haskell.