01LP | Logika programů | Rozsah výuky: | 2+2 | ||
---|---|---|---|---|---|
Přednášející (garant): | Typ předmětu: | S | Zakončení: | Z,ZK | |
Zodpovědná katedra: | 301 | Kreditů: | 4 | Semestr: | L |
Anotace:
Akční struktury, Milnerův jazyk CCS. Hennessy-Milnerova modální logika. Aplikace na jazyk WHILE - částečná korektnost programů. Minimální modální logika, úplnost a rozhodnutelnost. Věta o korespondenci a modální definovatelnost. Kleeneho věta o pevném bodě. Rekursivní rovnice v posetu. Modální m-kalkulus a m-rovnice, l- kalkulus a teorie typů. Redukce v l-kalkulu.
Osnovy přednášek:
1. | Množiny, relace, uspořádání | |
2. | Akční struktury, Milnerův jazyk CCS | |
3. | Hennessy-Milnerova modální logika | |
4. | Aplikace na jazyk WHILE - částečná korektnost programů | |
5. | Minimální modální logika | |
6. | Úplnost a rozhodnutelnost minimální modální logiky | |
7. | Věta o korespondenci a modální definovatelnost | |
8. | Kleeneho věta o pevném bodě. Rekursivní rovnice v posetu | |
9. | Modální ?-kalkulus | |
10. | Modální ?-rovnice | |
11. | ?-kalkulus a teorie typů | |
12. | Redukce v ?-kalkulu | |
13. | Návrh sémantiky programovacího jazyka | |
14. | Rezerva |
Osnovy cvičení:
1. | Množiny, relace, uspořádání | |
2. | Akční struktury, Milnerův jazyk CCS | |
3. | Hennessy-Milnerova modální logika | |
4. | Aplikace na jazyk WHILE - částečná korektnost programů | |
5. | Minimální modální logika | |
6. | Úplnost a rozhodnutelnost minimální modální logiky | |
7. | Věta o korespondenci a modální definovatelnost | |
8. | Kleeneho věta o pevném bodě. Rekursivní rovnice v posetu | |
9. | Modální ?-kalkulus | |
10. | Modální ?-rovnice | |
11. | ?-kalkulus a teorie typů | |
12. | Redukce v ?-kalkulu | |
13. | Návrh sémantiky programovacího jazyka | |
14. | Rezerva |
Literatura Č:
Literatura A:
Požadavky:
|
Předmět je zahrnut do těchto studijních plánů:
|
Stránka vytvořena 25. 2. 2002, semestry: Z/2001-2, Z/2002-3, L/2001-2, L/2002-3, připomínky k informační náplni zasílejte správci studijních plánů | Návrh a realizace: I. Halaška (K336), J. Novák (K336) |