Coronavirus - Informationen und Empfehlungen: https://colab.tuwien.ac.at/display/CORONA

192.098 Introduction to the Coq proof assistant
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

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

Inhalt der Lehrveranstaltung

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.

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

 

Methoden

Half lectures, half lab sessions

Prüfungsmodus

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

Vortragende

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Di.13:00 - 15:0005.05.2020Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Fr.13:00 - 15:0008.05.2020Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Mi.09:00 - 11:0013.05.2020Informatiklabor Frogger Übung
Fr.13:00 - 15:0015.05.2020Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Mi.09:00 - 11:0020.05.2020Informatiklabor Frogger Übung
Mi.09:00 - 11:0027.05.2020Informatiklabor Frogger Übung
Fr.13:00 - 15:0029.05.2020Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Mi.09:00 - 11:0003.06.2020Informatiklabor Frogger Übung
LVA wird geblockt abgehalten

Leistungsnachweis

Oral exam with a computer running the Coq proof assistant

LVA-Anmeldung

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

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Vorkenntnisse

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

Sprache

Englisch