Przedmiot ma na celu wprowadzenie do systemów typów znajdujących zastosowanie
w projektowaniu i implementacji języków programowania funkcyjnego oraz
obiektowego. Wykład oparty będzie na klasycznym już podręczniku Pierce'a
"Types and Programming Languages", a zajęcia w ramach pracowni towarzyszącej
wykładowi poświęcone będą implementacji wybranych systemów typów.
**Program:**
1. Typy proste (rachunek lambda z typami prostymi, rozszerzenia, normalizacja)
2. Efekty obliczeniowe w języku z typami prostymi (modyfikowalny stan, wyjątki, kontynuacje)
3. Podtypowanie
4. Typy iloczynowe i unijne
5. Typy rekurencyjne
6. Polimorfizm (rekonstrukcja typów, ML-polimorfizm, typy uniwersalne i egzystencjalne)
7. Systemy typów wyższego rzędu (F-omega)
8. Typy zależne
**Wymagania:** Logika dla informatyków Programowanie
