Typed lambda calculi, Curry and Church variants. Extensions of type systems. Questions of type
checking, type derivation, and type inhabitation.
Last update: T_KTI (14.05.2015)
Typovaný lambda kalkulus a jeho vztah k funkcionálnímu programovaní. Curryho a Churchova verze typování,
rozšíření typovacích systémů. Otázky typové kontroly, typového odvozování a obydlenosti typů.
Aim of the course -
Last update: RNDr. Jan Hric (07.06.2019)
To learn the theory of lambda-calculus, combinatory logic and explainn connections to functional programming.
Last update: RNDr. Jan Hric (23.04.2015)
Naučit teorii lambda-kalkulu, kombinatorické logiky a ukázat souvislosti s funkcionálním programováním.
Course completion requirements -
Last update: RNDr. Jan Hric (07.06.2019)
Oral exam on topics from lecture.
Last update: RNDr. Jan Hric (07.06.2019)
Na ústní zkoušce s přípravou prokázat znalost přednesených témat.
Literature -
Last update: T_KTI (14.05.2015)
Henk Barendregt, Erik Barensen: Introduction to Lambda Calculus, 1998, rev. 2000, 53 s. http://www.cs.ru.nl/E.Barendsen/onderwijs/T3/materiaal/lambda.pdf
Hendrik Pieter Barendregt: The Lambda Calculus: Its Syntax and Semantics. Elsevier, Amstredam, 1984. Rev. ed. 1998, 621 s. 0-444-86748-1
Henk Barendregt, Wil Dekkers, Richard Statman: Lambda Calculus with Types. Cambridge University Press, Cambridge, 2010. 682 s. (rev. 2013, 978-0-521-76614-2)
J. Roger Hindley, Jonathan P. Seldin: Lambda-Calculus and Combinators, an Introduction. Cambridge University Press, Cambridge, 2. vyd., 2008, 360 s. 978-0-521-89885-0 (1986. 359 s. 0-521-31839-4)
Last update: T_KTI (14.05.2013)
Henk Barendregt, Erik Barensen: Introduction to Lambda Calculus, 1998, rev. 2000, 53 s. http://www.cs.ru.nl/E.Barendsen/onderwijs/T3/materiaal/lambda.pdf
Hendrik Pieter Barendregt: The Lambda Calculus: Its Syntax and Semantics. Elsevier, Amstredam, 1984. Rev. ed. 1998, 621 s. 0-444-86748-1
Henk Barendregt, Wil Dekkers, Richard Statman: Lambda Calculus with Types. Cambridge University Press, Cambridge, 2010. 682 s. (rev. 2013, 978-0-521-76614-2)
J. Roger Hindley, Jonathan P. Seldin: Lambda-Calculus and Combinators, an Introduction. Cambridge University Press, Cambridge, 2. vyd., 2008, 360 s. 978-0-521-89885-0 (1986. 359 s. 0-521-31839-4)
Jiří Zlatuška: Lambda-kalkul. Masarykova univerzita, Brno, 1993. 264 s. 80-210-0826-1
Syllabus -
Last update: T_KTI (14.05.2015)
Typed lambda calculus. Extension of lambda calculus language with object types. Curry and Church variants of type systems, their axiomatic systems. Böhm trees, head normal form, approximations.
Extensions of Curry type systems with polymorphism, intersection types and recursive types.
Hierarchy of typed lambda calculus theories, lambda cube. Questions of type checking, type derivation, and type inhabitation. Strong normalization. Pure type systems. Relations of type systems with logic.
Last update: T_KTI (27.04.2016)
Typový lambda kalkul. Rozšíření jazyka lambda kalkulu o typy objektů. Curryho a Churchovy systémy, jejich rozšíření a varianty. Pravidla týkající se typů, axiomatické systémy. Böhmovy stromy, hlavová normální forma, aproximace.
Rozšíření Curryho typových systémů o polymorfismus, průnikové typy a rekurzivní typy.
Hierarchie teorií typového lambda kalkulu pro Churchovy systémy, lambda-cube. Polymorfizmus, typové proměnné a přiřazení hodnot typovým proměnným. Otázky typové kontroly, typového odvození a obydlenosti typů. Silná normalizace. Pure type systems. Vztah typů a logiky.