2012HS: 41570 Seminar Logic and Algebra

Coq Proof Assistant enables to produce verified formal proofs interactively by the means of automated “tactics.” With Coq, it is possible to describe precise specifications for programs and obtain code that is provably correct with respect to those specifications. Coq’s rich language also makes it suitable for use in formalizing mathematical statements and theories. Coq is currently one of the most important and influential computer environments for such tasks. The seminar intends to give a gentle introduction to Coq, both from the practical and the theoretical perspective. Textbook: Bertot Yves, Castéran Pierre. "Interactive Theorem Proving and Program Development". Springer, 2004. ISBN 978-3-540-20854-9 Copies of this book will be provided in the seminar.