📆 Schedule
Tuesday, 11th June 2024:
Lecture, 10:30–12:00
Tutorial, 12:15–13:30
Bonus, 14:30–15:30
Aula D
Wednesday, 12th June 2024:
Lecture, 11:30–13:30, Aula F
Bonus, 15:00–16:15, Aula I
Tutorial, 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:30
Aula L
If there is interest, we can schedule informal additional tutorial or
lecture sessions. The times are given in Verona local time (MEST).
📍 Location
All lectures and tutorials take place at the Dipartimento di Informatica:
Università di Verona, Cà Vignal 1–2, Strada le Grazie 15, Verona.
🌐 Remote participation
There was the option to participate in the minicourse remotely.
📝 Registration
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.
💡 Syllabus
- 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
Recordings are available
on YouTube
and also for direct download.
📖 References
- 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
- References for constructive commutative algebra
💬 Contact
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.