# 192.098 Introduction to the Coq proof assistant Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.\$(function(){PrimeFaces.cw("Tooltip","widget_j_id_21",{id:"j_id_21",showEffect:"fade",hideEffect:"fade",target:"isAllSteop"});});Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.\$(function(){PrimeFaces.cw("Tooltip","widget_j_id_23",{id:"j_id_23",showEffect:"fade",hideEffect:"fade",target:"isAnySteop"});}); 2020S

2020S, VU, 2.0h, 3.0EC, wird geblockt abgehalten

## Merkmale

• Semesterwochenstunden: 2.0
• ECTS: 3.0
• Typ: VU Vorlesung mit Übung

## Lernergebnisse

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

## This course gives an introduction to the Coq proof assistant:

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

### 4 lecture sessions

1. Introduction to Coq, Propositional Logic
2. Quantifiers, equality and all that
3. Inductive types
4. Inductive predicates

### 4 lab sessions

1. Your first proofs, propositional logic
2. First Order Logic, Higher Order Logic
3. Proofs by induction on nat
4. Proofs by induction on proofs

On line

Prüfungsimmanent

## Weitere Informationen

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

## LVA-Anmeldung

Von Bis Abmeldung bis
18.03.2020 10:00 04.05.2020 10:00 30.05.2020 10:00

## Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

## Vorkenntnisse

familiarity with first-order classical logic or with a functional programming language

Englisch