Kontynuacja przedmiotu [Weryfikacja programów w systemie Coq](https://zapisy.ii.uni.wroc.pl/offer/3475-weryfikacja-programow-w-systemie-coq/), która również jest realizowana w oparciu o podręcznik [Software Foundations](https://softwarefoundations.cis.upenn.edu). Tematy poruszane w ramach przedmiotu:
- formalizacja wybranych zagadnień teorii języków programowania opartych na rachunku lambda ([Programming Language Foundations](https://softwarefoundations.cis.upenn.edu/plf-current/index.html)),
- weryfikacja wybranych funkcyjnych algorytmów i struktur danych ([Verified Functional Algorithms](https://softwarefoundations.cis.upenn.edu/vfa-current/index.html)),
- weryfikacja wybranych programów w języku C z wykorzystaniem Verified Software Toolchain ([Verifiable C](https://softwarefoundations.cis.upenn.edu/vc-current/index.html)),
- jeśli czas pozwoli, spojrzenie na zastosowania współbieżnej logiki separacyjnej wyższego rzędu ([Iris Project](https://iris-project.org)).
Wymagania wstępne: znajomość Coqa na poziomie podręcznika [Logical Foundations](https://softwarefoundations.cis.upenn.edu/lf-current/index.html), logiki Hoare'a na poziomie [Programming Language Foundations](https://softwarefoundations.cis.upenn.edu/plf-current/index.html), a także logiki separacyjnej na poziomie [Separation Logic Foundations](https://softwarefoundations.cis.upenn.edu/slf-current/index.html).
Jest to przedmiot zaawansowany, wymagający czynnego udziału od uczestników. W szczególności, część wykładów może zostać zrealizowana w formie prezentacji studenckich.
