๐Ÿ“† 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

  1. 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
  2. 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 transcriptslides on infinite time Turing machinesnotes on toposes
  3. 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 transcriptAgda 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

Raw recordings are available at the following locations. Over the next few days, they will be properly cutted.

๐Ÿ“– References

๐Ÿ’ฌ 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.