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.

Beschreibung

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.

Allgemein

Sprache
Englisch
Copyright
This work has all rights reserved by the owner.

Verfügbarkeit

Zugriff
Unbegrenzt – wenn online geschaltet
Aufnahmeverfahren
Sie können diesem Kurs direkt beitreten.
Zeitraum für Beitritte
Unbegrenzt

Für Kursadministratoren freigegebene Daten

Daten des Persönlichen Profils
Anmeldename
Vorname
Nachname
E-Mail