Przedmiot będzie współprowadzony z D. Biernackim.
Jednym z powszechnie używanych obecnie
systemów wspomagających dowodzenie twierdzeń (nie tylko w środowisku akademickim) jest system Coq
(<http://coq.inria.fr/>), oparty na rachunku konstrukcji z definicjami
indukcyjnymi. Coq pozwala na definiowanie funkcji i predykatów, wyrażanie
twierdzeń matematycznych i specyfikacji oprogramowania, a także na
interakcyjne przeprowadzanie formalnych, weryfikowanych przez system dowodów
takich twierdzeń oraz generowanie certyfikowanego kodu.
Celem przedmiotu jest wyposażenie studentów w umiejętność praktycznego
wykorzystania systemu Coq do
modelowania i weryfikacji oprogramowania.
Przedmiot będzie prowadzony na podstawie materiałów Software Foundations (<https://softwarefoundations.cis.upenn.edu>), w szczególności rozdziałów Logical Foundations, Programming Language Foundations (fragmenty) i Separation Logic Foundations.
Wymagania:
-- Logika dla informatyków
-- przyda się znajomość jakiegoś języka
funkcyjnego
Zakres tematyczny:
1. Wprowadzenie do Coqa.
2. Logika Hoare'a.
3. Logika separacyjna.
4. Jeśli czas pozwoli, popatrzymy na Iris (https://iris-project.org/)
