Przedmiot stanowi wprowadzenie do formalnych technik opisu semantyki
(znaczenia) języków programowania oraz formalnych metod wnioskowania o
programach komputerowych. Omawiane na przedmiocie formalizmy znajdują
zastosowanie w projektowaniu i implementacji języków programowania, a także w
konstrukcji i weryfikacji oprogramowania. Wśród poruszanych tematów znajdą
się:
* definicje indukcyjne
* semantyka obliczeń imperatywnych, w tym semantyka operacyjna (naturalna) oraz denotacyjna (elementy teorii dziedzin)
* semantyka obliczeń z interakcją (wejście/wyjście i/lub procesy współbieżne, strukturalna semantyka operacyjna i etykietowane systemy przejść, koindukcja i bisymulacje)
* semantyka programów funkcyjnych, w tym rachunek lambda i jego rozszerzenia jako modelowy język funkcyjny (semantyka redukcyjna, maszyny abstrakcyjne, kontynuacje)
* systemy typów, w tym typy proste (typowanie syntaktyczne, terminacja obliczeń, relacje logiczne), polimorfizm parametryczny (darmowe twierdzenia), modularność (typowanie semantyczne), typy rekurencyjne (indeksowane relacje logiczne), równoważność kontekstowa programów, zaawansowane systemy typów (mutowalny stan, współbieżność, systemy typów i efektów).
W ramach ćwiczeń studenci będą rozwiązywać zadania teoretyczne ilustrujące i
poszerzające treści prezentowane na wykładzie.
**Prowadzący wykład:** Dariusz Biernacki i Filip Sieczkowski
**Wymagania wstępne:** Logika dla informatyków, Metody programowania,
Programowanie funkcyjne
**Literatura:**
1. _The Formal Semantics of Programming Languages: An Introduction._ Glynn Winskel. Foundation of Computing Series, MIT Press 1993, ISBN 978-0-262-23169-5.
2. _Semantics Engineering with PLT Redex._ Matthias Felleisen, Robert Bruce Findler, Matthew Flatt. The MIT Press 2009, ISBN 978-0262062756.
3. _Theories of Programming Languages._ John C. Reynolds. Cambridge University Press 1998, ISBN 978-0521594141.
4. _Types and Programming Languages._ Benjamin C. Pierce. The MIT Press 2001, ISBN 978-0262162098.
5. _Advanced Topics in Types and Programming Languages._ Benjamin C. Pierce (editor). The MIT Press 2004, ISBN 978-0262162289.
6. _Practical Foundations for Programming Languages (2nd edition)._ Robert Harper. Cambridge University Press 2016, ISBN 978-1107150300.
