University of Warsaw - Central Authentication System
Strona główna

Lambda calculus

General data

Course ID: 1000-2M02RL
Erasmus code / ISCED: 11.303 Kod klasyfikacyjny przedmiotu składa się z trzech do pięciu cyfr, przy czym trzy pierwsze oznaczają klasyfikację dziedziny wg. Listy kodów dziedzin obowiązującej w programie Socrates/Erasmus, czwarta (dotąd na ogół 0) – ewentualne uszczegółowienie informacji o dyscyplinie, piąta – stopień zaawansowania przedmiotu ustalony na podstawie roku studiów, dla którego przedmiot jest przeznaczony. / (0612) Database and network design and administration The ISCED (International Standard Classification of Education) code has been designed by UNESCO.
Course title: Lambda calculus
Name in Polish: Rachunek lambda
Organizational unit: Faculty of Mathematics, Informatics, and Mechanics
Course groups: (in Polish) Przedmioty 4EU+ (z oferty jednostek dydaktycznych)
(in Polish) Przedmioty obieralne na studiach drugiego stopnia na kierunku bioinformatyka
Elective courses for Computer Science
ECTS credit allocation (and other scores): 6.00 Basic information on ECTS credits allocation principles:
  • the annual hourly workload of the student’s work required to achieve the expected learning outcomes for a given stage is 1500-1800h, corresponding to 60 ECTS;
  • the student’s weekly hourly workload is 45 h;
  • 1 ECTS point corresponds to 25-30 hours of student work needed to achieve the assumed learning outcomes;
  • weekly student workload necessary to achieve the assumed learning outcomes allows to obtain 1.5 ECTS;
  • work required to pass the course, which has been assigned 3 ECTS, constitutes 10% of the semester student load.
view allocation of credits
Language: English
Type of course:

elective monographs
Prerequisites:

Languages, automata and computations 1000-214bJAO
Short description:

Introduction to lambda calculus as an abstract model of computation. Type-free lambda-calculus: properties of reduction, construction of models, undecidability.

Simply-typed and polymorphic lambda-calculi: normaliazation, expressiveness, connections to logic.
Full description:

1. Syntax of the untyped lambda-calculus. Alpha-conversion.

2. Properties of beta- and eta-reductions. Expressive power.

3. Denotational semantics for the untyped lambda-calculus.

4. Solvability and Boehm trees.

5. Simply-typed lambda-calculus. Strong normalization.

6. Semantics of simple types.

7. Formulas-as-types (the Curry-Howard isomorphism).

8. Combinatory logic.

9. Intersection types.

10. The polymorphic lambda-calculus (system F).

11. Decision problems for typed calculi.
Bibliography:

1. www.mimuw.edu.pl/~urzy/Lambda/rlambda.ps

2. Barendregt, H. Lambda Calculus, Elsevier, 1984.

3. Girard, J.-Y. Proofs and Types, Cambridge UP, 1989.
Learning outcomes:

Knowledge:

* Knows the lanuage of lambda-calculus and combinatory logic.

* Knows the methods of operational (reduction, Bohm trees) and

denotational semantics (Scott models) for the untyped calculus.

* Knows the expressive power of typed and untyped systems and their

relations to constructive logic.

* Knows various kinds of polymorphism (system F, intersection types).

Skills:

* Can express algorithms (function definitions) in the language of

lambda-terms and investigate their properties.

* Can analyze expressions with respect to typability.

Competences:

* Understands the relations between computational and logical phenomena.

* Understands theoretical foundations of semantics and functional programming.

* Understands the phenomenon of polymorphism.

Assessment methods and assessment criteria:

To pass the subject, one must pass the exercises and pass the exam.

The final grade will be determined on the basis of the exam.

To pass the exercises, it is necessary to submit homework.

It is the teacher who decides about passing the exercises.

Those who have completed their homework assignments and declared their readiness for the exam no later than January 7, can take the zero exam.

In the case of completing the course by a doctoral student, an additional criterion is to read a selected recent research article and discuss it

with the lecturer.

Classes in period "Winter semester 2023/24" (past)

Time span: 2023-10-01 - 2024-01-28
Selected timetable range:
Navigate to timetable
Type of class:
Classes, 30 hours more information
Lecture, 30 hours more information
Coordinators: Paweł Urzyczyn
Group instructors: Paweł Urzyczyn
Students list: (inaccessible to you)
Examination: Examination
Course descriptions are protected by copyright.
Copyright by University of Warsaw.
Krakowskie Przedmieście 26/28
00-927 Warszawa tel: +48 22 55 20 000 https://uw.edu.pl/ contact accessibility statement USOSweb 7.0.3.0 (2024-03-22)