Formal Type Theory
4
Algorithms and machine learning
Advanced studies
The course introduces basic concepts of programming language theory: operational semantics and type systems. The approach is strictly formal, with definitions and proofs carried out with the Coq proof assistant. The course proceeds from the basics of constructive logic in Coq to the theory and metatheory of simply typed lambda calculus and beyond. A strong background in logic (formal proofs) is required. Knowledge of functional programming, lambda calculus and/or compilers is recommended. Course exam Mon 14.12. at 16-19.
Lectures
| Time | Room | Lecturer | Date |
|---|---|---|---|
| Tue 12-14 | B222 | Lauri Alanko | 03.11.2009-10.12.2009 |
| Thu 12-14 | B222 | Lauri Alanko | 03.11.2009-10.12.2009 |
Exercise groups
| Time | Room | Instructor | Date | Observe |
|---|---|---|---|---|
| Thu 14-18 | B221 | Joel Kaasinen | 05.11.2009—05.11.2009 | |
| Thu 14-16 | B221 | Joel Kaasinen | 12.11.2009—12.11.2009 | |
| Thu 14-17 | B221 | Joel Kaasinen | 19.11.2009—26.11.2009 | |
| Thu 14-17 | B121 | Joel Kaasinen | 03.12.2009—03.12.2009 | |
| Thu 14-17 | B221 | Joel Kaasinen | 10.12.2009—10.12.2009 |
Ilmoittautuminen tälle kurssille alkaa tiistaina 13.10. klo 9.00.