[Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php) jest funkcyjnym językiem programowania opartym na teorii typów zależnych, a jednocześnie systemem wspomagającym dowodzenie twierdzeń opartym na paradygmacie "formuły jako typy, dowody jako programy". Tematem przedmiotu jest wprowadzenie do teorii języków programowania z wykorzystaniem systemu Agda, zrealizowane zgodnie z podręcznikiem [Programming Language Foundations in Agda](https://plfa.github.io/).
**Wymagania wstępne**
* Logika dla informatyków
* Metody programowania
Przedmiot prowadzony wspólnie z Małgorzatą Biernacką.
