Executing Proofs as Computer Programs

Aktuelles

  • Examination

    Dear all, an oral exam for the course is scheduled to take place on Tuesday 22.02.2022 in Room C123. In addition to answering questions, you will be asked to complete some basic proofs in the Agda proof assistant. Wishing you good luck and success in all your examinations.

    Zuletzt verändert: Di 15 Feb 2022 10:45

  • Online lectures

    Dear all, due to the current pandemic situation, let’s switch back to online lectures held in the same Zoom meeting room.

    Zuletzt verändert: Mo 29 Nov 2021 10:00

  • Zoom meeting room

    Dear all, the Zoom meeting room will be kept open during the next lectures, in case anyone has to or prefer to participate online due to the current COVID situation.

    Zuletzt verändert: So 21 Nov 2021 23:00

  • Classroom C123

    Dear all, the room C123 has been reserved for us. From Tuesday 9 November, we will have in-person lectures in C123. In the next two weeks, I’ll keep the Zoom meeting room open during the lecture, in case anyone missed this announcement.

    Zuletzt verändert: Mo 08 Nov 2021 16:00

Beschreibung

In response to the huge proofs that sometimes accompany landmark theorems nowadays, and that defy even teams of referees, the computer science and mathematics communities have developed proof assistants; these are purpose-built computer programs based on mathematical logic to formalize mathematical proofs and verify their correctness. Developing mathematics in a proof assistant is a difficult process, but it has advantage even beyond the correctness guarantee. For instance, some proof assistants allow users to obtain a certified computer program from the formalized proof.

The objective of the course is to encourage students to make use of proof assistants in their study of mathematics. During this course, we will use the Agda proof assistant for demonstration. In particular, we will study some examples of applying type-theoretic techniques, such as mutual inductive-recursive definitions and higher inductive types, in the development of mathematics.

Outline

The course is planed to cover the following topics:

  • Proof assistants and type theory
  • Proving and programming in Agda
  • Classical reasoning in intuitionistic type theory
  • Univalent mathematics
  • Mathematical applications of type-theoretic techniques

Literature

Time and place

Tuesday 10:15-12:00, starting on 19 October 2021

On 9, 16 and 23 November, the lectures took place in Room C123. From 30 November, we switch back to online lectures due to the pandemic situation.

Here is the link to the Zoom meeting room for the lectures:

Institut
Mathematisches Institut
Dozent:in
Kursteilnehmer:innen
9 von 10
Anmeldung

Fr 01 Okt 2021 00:00 – Do 31 Mär 2022 23:59

Abmeldung nur bis Do 31 Mär 2022 23:59

Material

Aktuell gibt es zu diesem Kurs keine Übungsblätter, oder nur Übungsblätter auf die Sie keinen Zugriff haben (z.B. aufgrund von Fristen bzgl. der Sichtbarkeit).

Material zum Kurs finden Sie hier: Material

Das Kursmaterial ist ohne Anmeldung frei zugänglich