Systemy typów (wykład i pracownia)
Instytut Informatyki UWr
Semestr zimowy 2010/11
Opis przedmiotu
Przedmiot ma na celu wprowadzenie do
systemów typów znajdujących zastosowanie w
projektowaniu i implementacji języków
programowania funkcyjnego oraz obiektowego, a
także, w mniejszym stopniu, przedstawienie ich
roli w logice. Wykład oparty jest na klasycznym
już podręczniku Pierce'a "Types and Programming
Languages", a zajęcia w ramach pracowni
towarzyszącej wykładowi poświęcone są
implementacji wybranych systemów typów.
Czas i miejsce
- Wykład: środa 10:15-12:00, sala 139
- Pracownia 1: wtorek 10:15-12:00, pracownia 108
- Pracownia 2: środa 12:15-14:00, pracownia 7
- Konsultacje: poniedziałek 10:15-12:00, pokój 327
|
Rozkład jazdy
|
Nr
|
Data
|
Zagadnienia
|
Do poczytania
|
Zadania
|
|
1.
|
06.10.2010
|
wstęp do wykładu (znaczenie typów i krótka
historia) oraz jego organizacja
formalne systemy wnioskowania i metody
dowodzenia ich własności na przykładzie
języka wyrażeń arytmetycznych
|
[Pie02]:1-4
|
lista 1
|
|
2.
|
20.10.2010
|
rachunek lambda jako język programowania
normalizacja, ewaluacja, CBV, CBN, maszyny abstrakcyjne
indeksy de Bruijna
|
[Pie02]:5-7
slajdy
|
lista 2
|
|
3.
|
27.10.2010
|
podstawowe własności systemów typów na przykładzie
wyrażeń arytmetycznych
rachunek lambda z typami prostymi
|
[Pie02]:8-10
|
|
|
4.
|
03.11.2010
|
dowód normalizacji dla rachunku lambda z
typami prostymi (metoda Taita)
rozszerzenia rachunku lambda z typami
prostymi (wyrażenia arytmetyczne i
logiczne, produkt i suma typów, rekursja
ogólna)
|
[Pie02]:11-12
|
|
|
5.
|
10.11.2010
|
efekty obliczeniowe w językach programowania:
semantyka operacyjna i typowanie referencji oraz wyjątków
|
[Pie02]:13-14
|
lista 3
|
|
6.
|
17.11.2010
|
kontynuacje
|
[FF06]:8, [Rey98]
[Plo75]
|
|
|
7.
|
24.11.2010
|
izomorfizm Curry'ego-Howarda
logika intuicjonistyczna vs. klasyczna
|
[SU06]:2-4
[Gri90]
|
|
|
8.
|
01.12.2010
|
podtypowanie
|
[Pie02]:15
|
|
|
9.
|
08.12.2010
|
semantyka koercyjna podtypowania
podtypowanie algorytmiczne
|
[Pie02]:16-17
|
lista 4
|
|
10.
|
15.12.2010
|
typy rekurencyjne
typy izo-rekurencyjne i ekwi-rekurencyjne
|
[Pie02]:20-21
|
|
|
11.
|
22.12.2010
|
rekonstrukcja typów
|
[Pie02]:22
|
lista 5
|
|
12.
|
12.01.2011
|
dowód poprawności algorytmu sprawdzającego
równoważność typów rekurencyjnych
|
[Pie02]:21
|
|
|
13.
|
19.01.2011
|
ML polimorfizm
algorytm Damasa-Milnera
|
[Pie02]:22
[Pit09]
|
|
|
14.
|
26.01.2011
|
polimorficzne referencje
rekursja polimorficzna
|
[Pie02]:22
[Pit09], [Tiu90]
|
|
Literatura podstawowa
-
[Pie02]
Pierce B., Types and Programming Languages, The MIT Press, 2002
-
[Pie05]
Pierce B., Advanced Topics in Types and Programming Languages, The MIT Press, 2005
Literatura uzupełniająca
-
[FF06]
Felleisen M., Flatt M., Programming Languages
and Lambda Calculi, Lecture Notes, 2006.
-
[GLT89]
Girard J.-Y., Lafont Y. and Taylor P., Proofs and Types, Cambridge University Press, 1989
-
[Gri90] Griffin T. G., Formulae-as-Types Notion of Control, POPL 1990.
-
[Gun92]
Gunter C., Semantics of Programming Languages: Structures and Techniques, MIT Press, 1992
-
[Har00]
Harper R., Type Systems for Programming Languages, Draft, CMU, 2000
-
[Har10]
Harper R., Practical Foundations for Programming Languages, Working Draft, CMU, 2010
-
[Hin97]
Hindley J. R., Basic Simple Type Theory, Cambridge University Press, 1997
-
[Mit96]
Mitchell J. C., Foundations for Programming Languages, The MIT Press, 1996
-
[Pit09]
Pitts A. M., Lecture Notes on Types, 2009.
-
[Plo75] Plotkin G. D., Call-by-Name,
Call-by-Value and the Lambda-Calculus, TCS,
Vol. 1, pp. 125-159, 1975
-
[Rey98]
Reynolds J. C., Theories of Programming Languages, Cambridge University Press, 1998
-
[SU06]
Sorensen M. H. and Urzyczyn P., Lectures on the Curry-Howard Isomorphism, Elsevier, 2006
-
[Tiu90]
Tiuryn J., Type Inference Problems: A Survey, LNCS 452, 1990.
|
|