Advanced Mechanized Reasoning in Coq (AMeRiCo)7.5 ECTS
(englische Bezeichnung: Advanced Mechanized Reasoning in Coq)
(Prüfungsordnungsmodul: Advanced Mechanized Reasoning in Coq)

Lehrveranstaltungen:

• • Advanced Mechanized Reasoning in Coq
    (Vorlesung mit Übung, 4 SWS, Tadeusz Litak, Di, 08:15 - 09:45, 01.151-128; Do, 16:15 - 17:45, 01.151-128)

Empfohlene Voraussetzungen:

Es wird empfohlen, folgende Module zu absolvieren, bevor dieses Modul belegt wird:

Praktische Semantik von Programmiersprachen (SS 2022)

Inhalt:

The aim of the module is to bridge the gap between introductory presentations such as the first two volumes of Software Foundations (covered in SemProg) and scalable, state-of-the-art Coq formalizations. From Coq itself, we plan to cover coinduction, typeclasses, termination metrics (Program Fixpoints vs. Equations), possibly also some aspects of MetaCoq, Ltac2 and SProp. When it comes to aspects of formalization and programming language semantics, we plan to discuss reasoning in the presence of binders (de Bruijn vs. locally nameless vs. HOAS approaches), formalization of separation logic, applications of logical relations (normalization, type safety, program equivalence), step indexing and partial evaluation. Details may be adjusted depending on background and preferences of the audience.

Lernziele und Kompetenzen:

Wissen

The students explain advanced aspects of both programming semantics and proof assistants, in particular Coq.

Verstehen

The students prove theorems using a proof assistant.

Anwenden

The students transfer proofs into programs and programs into proofs.

Analysieren

The students examine behaviour of complex programs using formal semantics

Evaluieren (Beurteilen)

The students evaluate the role played by logic and type theory in scientific approach to programming.

Erschaffen

The students provide formal semantics to a scalable programming language.

Literatur:

Online book "Software Foundations" http://www.cis.upenn.edu/~bcpierce/sf/
Online books by Adam Chlipala: "Certified Programming with Dependent Types" http://adam.chlipala.net/cpdt/ and "Formal Reasoning About Programs" http://adam.chlipala.net/frap/
Supplementary reading on the theory of programming: Types and Programming Languages Benjamin C. Pierce, The MIT Press
Supplementary reading on Coq: Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions Series: Texts in Theoretical Computer Science. An EATCS Series Bertot, Yves, Casteran, Pierre

Weitere Informationen:

Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan:

1. Artificial Intelligence (Master of Science)
   (Po-Vers. 2021s | TechFak | Artificial Intelligence (Master of Science) | Gesamtkonto | Wahlpflichtmodulbereich | Symbolic Artificial Intelligence | Advanced Mechanized Reasoning in Coq)

Studien-/Prüfungsleistungen:

Advanced Mechanized Reasoning in Coq (Prüfungsnummer: 31691)

(englischer Titel: Advanced Mechanized Reasoning in Coq)

Prüfungsleistung, mündliche Prüfung, Dauer (in Minuten): 30, benotet, 5 ECTS

Anteil an der Berechnung der Modulnote: 50.0 %

weitere Erläuterungen:
Die Modulnote setzt sich zu 50% aus dem Ergebnis einer 30-minütigen mündlichen Prüfung am Semesterende und zu 50% aus der Note für die Bearbeitung von fünf Übungsblättern zusammen. Gemäß Corona-Satzung wird als alternative Prüfungsform zur mündlichen Prüfung festgelegt: mündliche elektronische/digitale Distanzprüfung mit 30 Minuten Dauer.

Prüfungssprache: Deutsch und Englisch

Erstablegung: WS 2022/2023, 1. Wdh.: SS 2023 (nur für Wiederholer)

1. Prüfer:

Tadeusz Litak

Advanced Mechanized Reasoning in Coq (Prüfungsnummer: 31692)

Prüfungsleistung, Übungsleistung, benotet, 2.5 ECTS

Anteil an der Berechnung der Modulnote: 50.0 %

weitere Erläuterungen:
Die Modulnote setzt sich zu 50% aus dem Ergebnis einer 30-minütigen mündlichen Prüfung am Semesterende und zu 50% aus der Note für die Bearbeitung von fünf Übungsblättern zusammen. Gemäß Corona-Satzung wird als alternative Prüfungsform zur mündlichen Prüfung festgelegt: mündliche elektronische/digitale Distanzprüfung mit 30 Minuten Dauer.

Prüfungssprache: Deutsch und Englisch

Erstablegung: WS 2022/2023, 1. Wdh.: SS 2023

1. Prüfer:

Tadeusz Litak