**Overview:**
The Coq proof assistant provides a platform for interactive theorem proving
and for constructing certified programs, i.e., accompanied by a machine-
checked proof that the program satisfies its specification. Such a rigorous
approach to program correctness is crucial when it comes to the verification
of safety-critical software systems used in medicine, nuclear engineering or
transport. It is also an active research direction in compiler verification,
where the goal is to obtain a computer-checked certificate that the compiler
does not introduce bugs.
This seminar is a continuation of the course "Software foundations in Coq",
and its main objective is to provide the students with knowledge about program
certification in Coq, and in particular about formalized functional algorithms
and certiied compilers, but also to acquaint them with advanced formalization
techniques of the Coq proof assistant.
**Topics:**
* weak and strong program specification
* programming with dependent types
* verification of functional algorithms and data structures
* syntax and semantics of programming languages with binders ([POPLmark Challenge](https://www.seas.upenn.edu/~plclub/poplmark/poplmark.pdf))
* certified compilers, including [CompCert C](http://compcert.inria.fr/compcert-C.html)
* program extraction from proofs
* proof by reflection
* type classes
* general recursion
* crafting your own tactics with Ltac
**Prerequisites:**
It is assumed that the student has a basic working knowledge of Coq, logic,
functional programming, and the semantics of programming languages at the
level of [Software
Foundations](http://www.cis.upenn.edu/~bcpierce/sf/current/), taught at the
course Software foundations in Coq.
**Bibliography:**
* Benjamin C. Pierce. [Software Foundations](http://www.cis.upenn.edu/~bcpierce/sf/current/). 2017.
* 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/~plclub/poplmark/poplmark.pdf), 2005.
* Xavier Leroy, [Formal Verification of a Realistic Compiler](http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf), _Communications of the ACM_ , 52(7):107-115, 2009.
