Lambda calculus 1000-2M02RL
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.
Type of course
Prerequisites
Course coordinators
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 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.
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.
Additional information
Information on level of this course, year of study and semester when the course unit is delivered, types and amount of class hours - can be found in course structure diagrams of apropriate study programmes. This course is related to the following study programmes:
- Bachelor's degree, first cycle programme, Computer Science
- Master's degree, second cycle programme, Computer Science
Additional information (registration calendar, class conductors, localization and schedules of classes), might be available in the USOSweb system: