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ů.
Poslední úprava: T_KTI (14.05.2015)
Typed lambda calculi, Curry and Church variants. Extensions of type systems. Questions of type
checking, type derivation, and type inhabitation.
Cíl předmětu -
Poslední úprava: RNDr. Jan Hric (23.04.2015)
Naučit teorii lambda-kalkulu, kombinatorické logiky a ukázat souvislosti s funkcionálním programováním.
Poslední úprava: RNDr. Jan Hric (07.06.2019)
To learn the theory of lambda-calculus, combinatory logic and explainn connections to functional programming.
Podmínky zakončení předmětu -
Poslední úprava: RNDr. Jan Hric (07.06.2019)
Na ústní zkoušce s přípravou prokázat znalost přednesených témat.
Poslední úprava: RNDr. Jan Hric (07.06.2019)
Oral exam on topics from lecture.
Literatura -
Poslední úprava: 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
Poslední úprava: 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)
Sylabus -
Poslední úprava: 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.
Poslední úprava: 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.