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í
• Způsob výuky: prezenční
• Garant: RNDr. Jan Hric
• Třída: Informatika Mgr. - Teoretická informatika
• Kategorizace předmětu: Informatika > Programování, Teoretická informatika
• Korekvizity : NAIL078

Anotace

čeština

Poslední úprava: 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ů.

angličtina

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

čeština

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.

angličtina

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

čeština

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

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

angličtina

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

Oral exam on topics from lecture.

Literatura

čeština

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

angličtina

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

čeština

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.

angličtina

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.