Semantics of Programming Languages

Garant předmětu:

Tomáš Jakl

Přednášející:

Tomáš Jakl

Cvičící:

Tomáš Jakl

Předmět zajišťuje:

katedra teoretické informatiky

Anotace:

Cílem předmětu je uvést studenty do základů sémantiky programovacích jazyků, která je základem pro studium a implementaci programovacích jazyků.

Tyto techniky jsou také důležité pro verifikaci programů, implementaci optimalizací a obecný návrh programovacích jazyků.

Důraz bude na porovnání operační a denotační sémantiky. Použité techniky mají uplatnění i v případě analýzy jazyků daných pouze pomocí operační sémantiky.

Kurz umožní studentům získat potřebné dovednosti pro implementaci jazykových konstrukcí, ať už jejich popis pochází z teoretických nebo inženýrských zdrojů v literatuře.

Požadavky:

Osnova přednášek:

1. Přehled kurzu, motivace a vztah k praxi návrhu a implementace programovacích jazyků.

2. Pravidlová a strukturální indukce, vztah operační a denotační sémantiky.

3. Kontextuální a big-step sémantika.

4. Abstraktní stroje a kontinuace.

5. Typovaný lambda kalkulus s aritmetikou.

6. Sémantická a typová korektnost.

7. Sémantická úplnost.

8. Rekurzivní funkce a jazyk PCF.

9. Adekvátnost a kontextové lemma.

10. Otázka plné abstrakce (full abstraction) pro PCF.

11. Hoareův odvozovací systém I.

12. Hoareův odvozovací systém II.

13. Další témata.

Osnova cvičení:

1. Jazyk IMP- a jeho operační a denotační sémantika.

2. Rozšíření jazyka IMP- na jazyk IMP a jeho operační a denotační sémantika.

3. Základní vlastnosti CPOs, jejich konstrukce a CPO interpretace lambda kalkulu.

4. Logické relace, jakožto užitečná technika, s aplikacemi i mimo denotační sémantiku.

5. Ekvivalence operační a denotační sémantiky pro IMP.

6. Axiomatická sémantika.

Cíle studia:

Cílem předmětu je uvést studenty do základů sémantiky programovacích jazyků, která je základem pro studium a implementaci programovacích jazyků.

Tyto techniky jsou také důležité pro verifikaci programů, implementaci optimalizací a obecný návrh programovacích jazyků.

Studijní materiály:

1. Robert Harper: Practical Foundations for Programming Languages, 2nd Edition. Cambridge University Press, 2016. ISBN9781107150300.

2. Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, 1993. ISBN 9780262291453.

3. Tobias Nipkow , Gerwin Klein: Concrete Semantics, With Isabelle/HOL. Springer Cham, 2014. ISBN 978-3-319-10541-3.

4. Streicher, T: Domain-theoretic foundations of functional programming. World Scientific Publishing Company, 2006 ISBN 981-270-142-7.

5. Tennent, R. D.: Semantics of Programming Languages. ISBN 9780138055998.

6. Gunter, C. A.: Semantics of Programming Language. MIT Press, 1992. ISBN 9780262570954.

Poznámka:

předmět je vyučován v angličtině.

Další informace:

https://courses.fit.cvut.cz/NIE-SEM

Rozvrh na zimní semestr 2026/2027:

	06:00–08:0008:00–10:0010:00–12:0012:00–14:0014:00–16:0016:00–18:0018:00–20:0020:00–22:0022:00–24:00
Po
Út
St
Čt	místnost JP:B-571 Jakl T. 11:00–12:30 SUDÝ TÝDEN (přednášková par. 1 paralelka 101) Jugoslávských partyzánů 3místnost JP:B-570 Jakl T. 14:30–16:00 (přednášková par. 1) Jugoslávských partyzánů 3
Pá

Rozvrh na letní semestr 2026/2027:

Rozvrh není připraven

Předmět je součástí následujících studijních plánů:

• Master specialization Software engineering, program ANI (volitelný předmět)
• Master specialization Embedded systems (volitelný předmět)
• Master program ANIE for the phase of study without specialisation (volitelný předmět)
• Quantum Informatics (volitelný předmět)
• Master specialization Computer Security, Version 2026 (VO)
• Master programme, for the phase of study without specialisation, ver. for 2026 and higher (VO)
• Master specialization Computer Systems and Networks, in English, 2026 (VO)
• Master specialization Computer Science, in English, 2026 (VO)
• Master specialization Programming Languages, in English, 2026 (PS)