Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage to understand and use the Coq proof assistant; in particular to formalize propositional logic, quantifiers inductive types and inductive predicates
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem, or homotopy type theory), and teaching.
The first course will take place on-line as scheduled: - Tuesday May 5, 2020, 13:00-15:00
On line
The course will be held blocked May-June
Ects Breakdown 8.0 h attendance of lecture (4 days x 2h) 8.0 h self study at home (4 x 2h) 8.0 h attendance to lab sessions (4 days x 2h) 8.0 h homework (4 x 2h)32.0 h project preparation 1.0 h project presentation 9.0 h preparation for oral exam 1.0 h oral exam-----------------------------------------------75.0 h = 3 Ects
To be decided
familiarity with first-order classical logic or with a functional programming language