Summer school
The 15th Panhellenic Logic Symposium was the first to add a summer school before the main schedule, in order to familiarise students with Model Theory and Descriptive Set Theory.
I was pleasantly surprised to see plenty of participants, with their home institutions spanning from the neighbouring Turkey to the faraway USA - most of them being early PhD students. I’m glad for the interesting discussions that arose, where the coolest one I heard of was the belief that “indirect existence is the shadow of a constructive existence”.
My talk
After the main talks, there were a few student talks and I presented on the following topic:
From Martin-Löf to Homotopy Type Theory: Live-Coding Alternative Foundations
Abstract: Can we do mathematics natively within a computer? This short talk presents dependent type theory as an alternative foundational framework to set theory, explored live through the Agda proof assistant. We will briefly map the transition from classical logic to Martin-Löf Type Theory (MLTT), by exploring the Curry-Howard correspondence, dependent types (Π and Σ), and the expressive power of inductive type families used for generating all kinds of mathematical structures. The session peaks with an interactive look at the identity type, sketching how computational equality opens the door to Homotopy Type Theory (HoTT). Ultimately, the goal is simply to share the practical joy of this “new way” of doing mathematics, by showing how Agda turns proof-writing into a guided, interactive dialogue with the compiler.
(^ clicking in the box above will reveal the abstract)
Out of the 25-ish participants, a couple had some programming experience and even fewer had some exposure to type theory. This made my presentation a great learning experience when it comes to assessing an audience’s background, as I had assumed a broader exposure to basic programming (and other student speakers could afford to assume a much more extensive background). Admittedly, the planned extent of my talk was ambitious and I felt I could do better with regards to the amount of material actually covered. However, there were more than a handful questions asked (and answered) - which usually is a good metric for the success of a talk.
The main event starts next week :)