- Minicourse by Ingo Blechschmidt at the University of Verona
**Exercise sheets**• Agda templates**Recordings**- Contact Ingo on Telegram
- Informal Telegram group for the minicourse

Tuesday, 11th June 2024:Lecture, 10:30โ12:00 Tutorial, 12:15โ13:30 Bonus, 14:30โ15:30Aula DWednesday, 12th June 2024:Lecture, 11:30โ13:30,Aula FBonus, 15:00โ16:15,Aula ITutorial, 16:30โ18:30,Aula I~~Sala riunioni secondo piano~~Thursday, 13th June 2024:Bonus, 11:00โ12:30, Aula H Lecture, 13:30โ15:00 Tutorial, 15:15โ16:30Aula L

If there is interest, we can schedule informal additional tutorial or lecture sessions. The times are given in Verona local time (MEST).

All lectures and tutorials take place at the Dipartimento di Informatica: Universitร di Verona, Cร Vignal 1โ2, Strada le Grazie 15, Verona.

There was the option to participate in the minicourse remotely.

No registration is required, but for organizational purposes, we kindly request an informal notification of your intent to attend via mail. If you indicate in your mail your scientific background, I will try to tailor the course to your interests.

**Construction**—a flavor of mathematics centered around informative constructions

proof by contradiction and proof of contradiction • law of excluded middle • constructive reading of logical connectives • decidability • Brouwerian counterexamples • geometric interpretation

raw transcript • notes (Section I) • transcript of the first Agda session**Realizability**—extracting programs from constructive proofs

connection between constructive and computable mathematics • basic definitions and examples • realizers of negated statements • soundness theorem • induction by recursion • cut by composition • Markov's principle • a counterexample to the axiom of choice • automatic continuity • infinite time Turing machines

raw transcript • slides • slides on infinite time Turing machines • notes on toposes**Double negation**—turning classical proofs into constructive proofs

a classical logic fairy tale • sarcastic interpretation of classical logic • embedding classical into constructive mathematics • infinite pigeonhole principle • well quasi-orders • escaping the continuation monad • Barr's theorem

raw transcript • notes (Section II) • Agda code for Dickson's lemma

All material will be accompanied by matching exercises and, for those
interested in that, a **tutorial on Agda**—the programming
and proof language—for exploring program extraction practically.

Recordings are available on YouTube and also for direct download.

- Andrej Bauer. Five stages of accepting constructive mathematics (video), 2013.
- Andrej Bauer. Realizability as the connection between computable and constructive mathematics (pdf), 2005.
- Andrej Bauer. Intuitionistic mathematics and realizability in the physical world (pdf), 2012.
- Ingo Blechschmidt. The curious world of constructive mathematics (pdf), 2022.
- Ingo Blechschmidt. Extraction of programs from proofs (pdf), 2022.
- Liron Cohen, Sofia Faro and Ross Tate. The effects of effects on constructivism (pdf), 2019.
- Thierry Coquand. Computational content of classical logic (pdf), 2009.
- Laura Fontanella. Realizability and the axiom of choice (pdf), 2020.
- Ariel Kellison. A machine-checked direct proof of the SteinerโLehmus theorem (pdf), 2021.
- Alexandre Miquel. An introduction to Kleene realizability (pdf), 2016.
- Jaap van Oosten. Realizability: a historical essay (web), 2000.
- Jaap van Oosten. Realizability: an introduction to its categorical side (web), 2008.
- Thomas Streicher. Realizability (pdf), 2018.
- References for Agda
- References for synthetic computability theory: slides of Andrej Bauer, Andrej Bauer again, Yannick Forster, Dominik Kirst

mail: iblech@speicherleck.de

phone: +49 176 95110311 (also Telegram)

*This minicourse was organized by Peter Schuster with support from
Alexander Mai, whose work I greatly acknowledge.*