FI:IA011 Sémantiky progr. jazyků - Informace o předmětu

IA011 Sémantiky programovacích jazyků

Rozsah

2/1/0. 3 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: z.

Vyučující

prof. RNDr. Antonín Kučera, Ph.D. (přednášející)
Mgr. Bc. Tomáš Janík (pomocník)

Garance

prof. RNDr. Antonín Kučera, Ph.D.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Antonín Kučera, Ph.D.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

Rozvrh

Po 13:00–15:50 B410

Předpoklady

Předpokladem je znalost základních pojmů teorie množin a formální logiky (pravdivá a dokazatelná tvrzení, odvozovací systémy, korektnost a úplnost odvozovacích systémů, apod.)

Omezení zápisu do předmětu

Předmět je nabízen i studentům mimo mateřské obory.

Mateřské obory/plány

• Analýza a zpracování obrazu (program FI, N-VIZ)
• Aplikovaná informatika (program FI, N-AP)
• Bezpečnost informačních technologií (angl.) (program FI, N-IN)
• Bezpečnost informačních technologií (program FI, N-IN)
• Bioinformatika a systémová biologie (program FI, N-UIZD)
• Bioinformatika (program FI, N-AP)
• Computer Games Development (program FI, N-VIZ_A)
• Computer Graphics and Visualisation (program FI, N-VIZ_A)
• Computer Networks and Communications (program FI, N-PSKB_A)
• Cybersecurity Management (program FI, N-RSSS_A)
• Diskrétní algoritmy a modely (program FI, N-TEI)
• Formální analýza počítačových systémů (program FI, N-TEI)
• Grafický design (program FI, N-VIZ)
• Graphic Design (program FI, N-VIZ_A)
• Hardware Systems (program FI, N-PSKB_A)
• Hardwarové systémy (program FI, N-PSKB)
• Image Processing and Analysis (program FI, N-VIZ_A)
• Informační bezpečnost (program FI, N-PSKB)
• Informační systémy (program FI, N-IN)
• Information Security (program FI, N-PSKB_A)
• Kvantové a jiné neklasické výpočetní modely (program FI, N-TEI)
• Paralelní a distribuované systémy (program FI, N-IN)
• Počítačová grafika a vizualizace (program FI, N-VIZ)
• Počítačová grafika (program FI, N-IN)
• Počítačové sítě a komunikace (program FI, N-IN)
• Počítačové sítě a komunikace (program FI, N-PSKB)
• Počítačové systémy (program FI, N-IN)
• Principy programovacích jazyků (program FI, N-TEI)
• Programovatelné technické struktury (angl.) (program FI, N-IN)
• Programovatelné technické struktury (program FI, N-IN)
• Řízení kyberbezpečnosti (program FI, N-RSSS)
• Řízení vývoje služeb (program FI, N-RSSS)
• Řízení vývoje softwarových systémů (program FI, N-RSSS)
• Services Development Management (program FI, N-RSSS_A)
• Služby - výzkum, řízení a inovace (angl.) (program FI, N-AP)
• Služby - výzkum, řízení a inovace (program FI, N-AP)
• Sociální informatika (program FI, B-AP)
• Software Systems Development Management (program FI, N-RSSS_A)
• Software Systems (program FI, N-PSKB_A)
• Softwarové systémy (program FI, N-PSKB)
• Strojové učení a umělá inteligence (program FI, N-UIZD)
• Teoretická informatika (program FI, N-IN)
• Učitelství výpočetní techniky pro střední školy (program FI, N-SS) (2)
• Umělá inteligence a zpracování přirozeného jazyka (program FI, N-IN)
• Vývoj počítačových her (program FI, N-VIZ)
• Zpracování a analýza rozsáhlých dat (program FI, N-UIZD)
• Zpracování obrazu (program FI, N-AP)
• Zpracování přirozeného jazyka (program FI, N-UIZD)

Cíle předmětu

Úvodní kurs do teorie formálních sémantik programovacích jazyků, pokrývající základní paradigmata (operační, denotační, axiomatická) a vztahy mezi nimi. Okrajově jsou zmíněny další přístupy (temporalní logiky). Hlavním cílem kurzu je:

Výstupy z učení

Student bude:
chápat a rozlišovat definice formálních sémantik programovacích jazyků;
formálně argumentovat vlastnosti programů;
schopen číst a použít formule základní temporální logiky.

Osnova

• Sémantiky programovacích jazyků, základní paradigmata (operační, denotanční a axiomatická sémantika).
• Strukturální operační sémantika a její varianty. Ekvivalence sémantik.
• Denotační sémantika. Pojem CPO, spojité funkce mezi CPO. Věta o pevném bodě a její aplikace, sémantika rekurze. Ekvivalence operační a denotanční sémantiky.
• Axiomatická sémantika. Hoareův odvozovací systém, jeho korektnost a úplnost.
• Temporální logiky, sémantika neukončených a paralelních programů.

Literatura

• SCHMIDT, David A. The structure of typed programming languages. Cambridge: MIT Press, 1994, viii, 367. ISBN 0262193493. info
• WINSKEL, Glynn. The formal semantics of programming languages : an introduction. Cambridge: MIT Press, 1993, xi, 361 s. ISBN 0-262-23169-7. info

Výukové metody

Přednášky, cvičení.

Metody hodnocení

Přednáška: 2 hodiny týdně. Cvičení: 1 hodina týdně.
Zkouška je písemná.

Informace učitele

http://www.fi.muni.cz/usr/kucera/teaching.html

Další komentáře

Studijní materiály
Předmět je vyučován každoročně.

• Statistika zápisu (nejnovější)
  
• Permalink: https://is.muni.cz/predmet/fi/jaro2024/IA011