Formal Type Theory

Algoritmit ja koneoppiminen
Syventävät opinnot
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.
Vuosi Lukukausi Päivämäärä Periodi Kieli Vastuuhenkilö
2009 syksy 03.11-10.12. 2-2 Englanti


Aika Huone Luennoija Päivämäärä
Ti 12-14 B222 Lauri Alanko 03.11.2009-10.12.2009
To 12-14 B222 Lauri Alanko 03.11.2009-10.12.2009


Group: 1
Aika Huone Ohjaaja Päivämäärä Huomioitavaa
To 14-18 B221 Joel Kaasinen 05.11.2009—05.11.2009
To 14-16 B221 Joel Kaasinen 12.11.2009—12.11.2009
To 14-17 B221 Joel Kaasinen 19.11.2009—26.11.2009
To 14-17 B121 Joel Kaasinen 03.12.2009—03.12.2009
To 14-17 B221 Joel Kaasinen 10.12.2009—10.12.2009

Ilmoittautuminen tälle kurssille alkaa tiistaina 13.10. klo 9.00.