Wykład będzie przeglądem wybranych koncepcji, wokół których zbudowane są systemy typów współczesnych języków programowania. Nacisk będzie położony przede wszystkim na teoretyczne aspekty systemów typów. Będziemy szukać odpowiedzi na pytania takie jak:
- Co to znaczy, że system typów jest poprawny?
- Jak pokazać poprawność systemu typów?
- Co tak naprawdę znaczą typy?
- Jak zaprojektować system typów, by nie zrobić czegoś głupiego?
### Wymagania
- Zaliczone: Logika dla Informatyków i Metody Programowania.
- Znajomość jakiegoś silnie typowanego języka funkcyjnego (np. OCaml, Haskell).
- Zamiłowanie do matematycznej elegancji.
### Program
1. Składnia i semantyka operacyjna
2. Typy proste
3. Polimorfizm parametryczny
4. Relacje logiczne, parametryczność i abstrakcja danych
5. Typy rekurencyjne
6. Relacje logiczne indeksowane krokami
7. Podtypowanie
8. Systemy typów i efektów
