Lambda-kalkulus a funkcionální programování 2 - NAIL079

• Anglický název: Lambda Calculus and Functional Programming 2
• Zajišťuje: Katedra teoretické informatiky a matematické logiky (32-KTIML)
• Fakulta: Matematicko-fyzikální fakulta
• Platnost: od 2020
• Semestr: letní
• E-Kredity: 4
• Rozsah, examinace: letní s.:2/1, Z+Zk [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• Stav předmětu: vyučován
• Jazyk výuky: čeština, angličtina
• Způsob výuky: prezenční
• Garant: RNDr. Jan Hric
• Vyučující: RNDr. Jan Hric
• Třída: Informatika Mgr. - Teoretická informatika
• Kategorizace předmětu: Informatika > Programování, Teoretická informatika
• Korekvizity : NAIL078

Anotace

čeština

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)

angličtina

Typed lambda calculi, Curry and Church variants. Extensions of type systems. Questions of type checking, type derivation, and type inhabitation.

Poslední úprava: T_KTI (14.05.2015)

Cíl předmětu

čeština

Naučit teorii lambda-kalkulu, kombinatorické logiky a ukázat souvislosti s funkcionálním programováním.

Poslední úprava: Hric Jan, RNDr. (23.04.2015)

angličtina

To learn the theory of lambda-calculus, combinatory logic and explainn connections to functional programming.

Poslední úprava: Hric Jan, RNDr. (07.06.2019)

Podmínky zakončení předmětu

čeština

Na ústní zkoušce s přípravou prokázat znalost přednesených témat.

Poslední úprava: Hric Jan, RNDr. (07.06.2019)

angličtina

Oral exam on topics from lecture.

Poslední úprava: Hric Jan, RNDr. (07.06.2019)

Literatura

čeština

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.2013)

angličtina

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)

Poslední úprava: T_KTI (14.05.2015)

Sylabus

čeština

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 (27.04.2016)

angličtina

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.

Poslední úprava: T_KTI (14.05.2015)