Subjects

Your browser does not support JavaScript, or its support is disabled. Some features may not be available.

Lambda Calculus and Functional Programming 2 - NAIL079

Title:	Lambda-kalkulus a funkcionální programování 2
Guaranteed by:	Department of Theoretical Computer Science and Mathematical Logic (32-KTIML)
Faculty:	Faculty of Mathematics and Physics
Actual:	from 2020
Semester:	summer
E-Credits:	4
Hours per week, examination:	summer s.:2/1, C+Ex [HT]
Capacity:	unlimited
Min. number of students:	unlimited
4EU+:	no
Virtual mobility / capacity:	no
State of the course:	taught
Language:	Czech, English
Teaching methods:	full-time
Teaching methods:	full-time

Guarantor:	RNDr. Jan Hric
Class:	Informatika Mgr. - Teoretická informatika
Classification:	Informatics > Programming, Theoretical Computer Science
Co-requisite :	NAIL078

Opinion survey results Examination dates SS schedule Noticeboard

Annotation -

Last update: 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.

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.

Course completion requirements -

Last update: RNDr. Jan Hric (07.06.2019)

Oral exam on topics from lecture.

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)

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.