PředmětyPředměty(verze: 830)
Předmět, akademický rok 2018/2019
   Přihlásit přes CAS
Lambda-kalkulus a funkcionální programování II - NAIL079
Anglický název: Lambda Calculus and Functional Programming II
Zajišťuje: Katedra teoretické informatiky a matematické logiky (32-KTIML)
Fakulta: Matematicko-fyzikální fakulta
Platnost: od 2015
Semestr: letní
E-Kredity: 5
Rozsah, examinace: letní s.:2/1 Z+Zk [hodiny/týden]
Počet míst: neomezen
Minimální obsazenost: neomezen
Stav předmětu: vyučován
Jazyk výuky: čeština, angličtina
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 -
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ů.
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.

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

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.

 
Univerzita Karlova | Informační systém UK