Semantyka języków programowania
Terminarz
Wykład odbywa się we wtorki o godz. 10:15 w sali 105. Po
wykładzie o godz. 12:15 odbywają się albo ćwiczenia w sali
105, albo pracownia w sali 108, zgodnie z poniższym
terminarzem.
|
Plan zajęć
| Data |
Zajęcia |
Temat |
Notatki |
Literatura |
Kod |
Zadania |
| 08.10.2013 |
Wykład 1 |
Organizacja przedmiotu
Wprowadzenie do semantyki języków programowania
Modelowy język imperatywny IMP
Składnia abstrakcyjna i konkretna
Semantyka naturalna
|
|
[Win93]:2
[NN07]:1, 2.1 |
|
Lista zadań nr 1 |
|
|
|
|
|
|
|
| 15.10.2013 |
Wykład 2 |
Indukcja matematyczna, indukcja dobrze ufundowana,
indukcja strukturalna
Elementy metateorii języka IMP
|
|
[Win93]:3
[NN07]:1, 2.1 |
|
Lista zadań nr 2 |
|
Pracownia |
|
|
|
|
|
| 22.10.2013 |
Wykład 3 |
Definicje indukcyjne
Cukier syntaktyczny
Błędy arytmetyczne
Równoważność obserwacyjna programów
|
|
[Win93]:4
[Rey98]:2.6-2.8 |
|
Lista zadań nr 3 |
|
Ćwiczenia |
|
|
|
|
|
| 29.10.2013 |
Wykład 4 |
Strukturalna semantyka operacyjna małych kroków
|
|
[NN07]:2.2-2.3
|
|
Lista zadań nr 4 |
|
Ćwiczenia |
|
|
|
|
|
| 05.11.2013 |
Wykład 5 |
Konteksty ewaluacyjne i semantyka redukcyjna
Maszyna abstrakcyjna
|
|
[Pit02]:1.2
|
|
Lista zadań nr 5
|
|
Ćwiczenia |
|
|
|
|
|
| 12.11.2013 |
Wykład 6 |
Semantyka denotacyjna
Elementy teorii dziedzin
|
|
[Win93]:5
[NN07]:5
|
|
Lista zadań nr 6
|
|
Pracownia |
|
|
|
|
|
| 19.11.2013 |
Wykład 7 |
Elementy teorii dziedzin, c.d.
Semantyka denotacyjna porażek oraz instrukcji wyjścia
|
|
[Win93]:8
[Rey98]:2.2-2.3, 5.1-5.2
|
|
Lista zadań nr 7
|
|
Ćwiczenia |
|
|
|
|
|
| 26.11.2013 |
Wykład 8 |
Izomorfizmy dziedzin
Semantyka denotacyjna porażek oraz wejścia/wyjścia w dziedzinie wznowień
Semantyka kontynuacyjna
Kontynuacje sukcesu i porażki
|
|
[Rey98]:5.3-5.7
|
|
Lista zadań nr 8
|
|
Ćwiczenia |
|
|
|
|
|
| 03.12.2013 |
Wykład 9 |
Bloki i procedury
Zasięg dynamiczny i statyczny
Środowiska
|
|
[NN07]:3.2, 6.1
|
|
Lista zadań nr 9
|
|
Pracownia |
|
|
|
|
|
| 10.12.2013 |
Wykład 10 |
Etykietowane systemy przejść
Semantyka operacyjna wejścia/wyjścia
Równoważność obliczeń nieskończonych -- bisymulacje
|
|
[Pit02]:6.1-6.2
|
|
Lista zadań nr 10
|
|
Pracownia |
|
|
|
|
|
| 17.12.2013 |
Wykład 11 |
Koindukcyjna charakteryzacja nieterminacji
Semantyka obliczeń niedeterministycznych
Niedeterminizm ograniczony i dziedziny potęgowe
|
|
[Rey98]:7
|
|
Lista zadań nr 11
|
|
Ćwiczenia |
|
|
|
|
|
| 14.01.2014 |
Wykład 12 |
Semantyka procesów współbieżnych ze wspólną pamięcią
Interferencja procesów, sekcje krytyczne, wzajemne wykluczanie, blokada, sprawiedliwość
Semantyka wznowień oraz semantyka śladów
|
|
[Rey98]:8
|
|
Lista zadań nr 12
|
|
Ćwiczenia |
|
|
|
|
|
| 21.01.2014 |
Wykład 13 |
Semantyka operacyjna i denotacyjna gorliwego języka
funkcyjnego
|
|
[Rey98]:10-11
[Win93]:9-10
|
|
Lista zadań nr 13
|
|
Ćwiczenia |
|
|
|
|
|
| 28.01.2014 |
Wykład 14 |
Kontynuacje w językach funkcyjnych
Semantyka operacyjna i denotacyjna leniwego języka funkcyjnego
|
|
[Rey98]:12,14
[Win93]:9-10
|
|
Lista zadań nr 14
|
|
Ćwiczenia |
|
|
|
|
|
| 28.01.2014 |
Wykład 15 |
Strategia ewaluacji "call by need"
|
|
[Rey98]:14
|
|
|
|
Pracownia |
|
|
|
|
|
|