Przedmiot stanowi wprowadzenie do formalnych technik opisu semantyki
(znaczenia) języków programowania. Omawiane na przedmiocie formalizmy znajdują
zastosowanie w projektowaniu i implementacji języków programowania, a także we wnioskowaniu o programach. Wśród poruszanych tematów znajdą
się:
* semantyka obliczeń imperatywnych, w tym semantyka operacyjna oraz denotacyjna (włączając 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 (rachunek lambda jako modelowy język funkcyjny, semantyka redukcyjna, maszyny abstrakcyjne, kontynuacje)
* jeżeli czas pozwoli: PCF (semantyka operacyjna i denotacyjna: poprawność i adekwatność, kontekstowa równoważność, _full abstraction_).
W ramach ćwiczeń studenci będą rozwiązywać zadania teoretyczne ilustrujące i
poszerzające treści prezentowane na wykładzie. Dodatkowo, zarówno na wykładzie jak i na ćwiczeniach mogą pojawić się zagadnienia implementacyjne do zrealizowania w języku OCaml.
**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. [Lecture Notes on Semantics of Programming Languages](https://www.cl.cam.ac.uk/teaching/2001/Semantics/sempl.ps.gz). Andrew Pitts. University of Cambridge.
5. [Lecture Notes on Denotational Semantics](https://www.cl.cam.ac.uk/teaching/1819/DenotSem/DenotSem2018.pdf). Andrew Pitts. University of Cambridge.
