Wartungsarbeiten: File-Server So/Mo 26. Mai 22:00 - 27. Mai 07:00 | Aufgrund von Wartungsarbeiten an den File-Servern können in diesem Zeitraum keine Dateien hochgeladen werden. Die Dateien auf ILIAS können aber weiterhin heruntergeladen/angesehen werden.
Icon Course

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.

Description

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.

General

Language
English
Copyright
This work has all rights reserved by the owner.

Availability

Access
Unlimited
Admittance
You can join this course directly.
Registration Period
Unlimited

Visible Personal Data for Course Administrators

Data Types of the Personal Profile
Username
First Name
Last Name
E-Mail

Additional Information

Permanent Link