System Coq, ktory łączy w sobie język programowania z interaktywnym systemem
wspomagającym dowodzenie twierdzeń, pozwala na konstruowanie certyfikowanego
oprogramowania, a więc takiego, ktoremu towarzyszy zweryfikowany przez
komputer dowod poprawności. Tak rygorystyczne podejście do poprawności
oprogramowania znajduje szczegolne uzasadnienie w przypadku projektowania i
implementacji językow programowania. To od tego czy semantyka języka jest
poprawna oraz czy kompilator zachowuje semantykę zależy poprawne wykonanie
programow napisanych w tym języku i na nic zda się weryfikacja samych
programow, gdy kompilator zawiera błędy.
Przedmiot stanowi rozwinięcie wykładu "Podstawy językow programowania w
systemie Coq", a jego celem jest wprowadzenie studentow do zagadnień
związanych z certyfikacją kompilatorow w systemie Coq, łącząc w sobie typowe
seminarium z projektem formalizacyjnym. W części seminaryjnej omowiona
zostanie podstawowa literatura, a także wybrane najnowsze prace dotyczące
certyfikowanej kompilacji językow programowania. W części projektowej
postawimy sobie zespołowe zadanie formalizacyjne, polegające na skonstruowaniu
(fragmentow) certyfikowanego kompilatora wybranego języka programowania.
Literatura:
* Benjamin C. Pierce. [Software Foundations](http://www.cis.upenn.edu/%7Ebcpierce/sf/current/). 2015.
* Adam Chlipala. [Certified Programming with Dependent Types](http://adam.chlipala.net/cpdt/). _The MIT Press_ , 2013.
* Yves Bertot, Pierre Casteran. [Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions](http://www.cse.chalmers.se/research/group/logic/TypesSS05/resources/coq/CoqArt/). _Springer_ , 2004.
* Brian E. Aydemir et al., [The POPLmark Challenge](https://www.seas.upenn.edu/%7Eplclub/poplmark/poplmark.pdf), 2005.
* Xavier Leroy. A formally verified compiler back-end. _Journal of Automated Reasoning_ , 43(4):363--446, 2009. [CompCert's website](http://compcert.inria.fr/).
* [MLCompCert](http://pauillac.inria.fr/~dargaye/mlcompcert.html). Zaynah Dargaye.
* Adam Chlipala. A certified type-preserving compiler from lambda calculus to assembly language. _PLDI 2007._
* Adam Chlipala. A verified compiler for an impure functional language. _POPL 2010.
_
* Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis. Pilsner: a compositionally verified compiler for a higher-order imperative language. _ICFP 2015._
* Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish. A new verified compiler backend for CakeML. _ICFP 2016_. [CakeML's website](https://cakeml.org/).
