LogSem Seminar, 2025
A seminar series on program verification, logic, semantics, type theory, proof assistants and related topics.
The presentation format is pretty open. Everyone is welcome (and encouraged!) to present previous/current work, explain interesting papers, give tutorial talks on topics they find worth sharing. Typically, it is a 45 min presentation + 15 min discussion, but, of course, flexible.
We meet on Mondays from 13:00 to 15:00. Currently all meetings are either in-person (in Ada-333 unless otherwise stated) or virtual on Zoom.
This meeting is organized by Alejandro Aguirre and Sergei Stepanenko.
A preliminary schedule is available below.
| Date | Who | Topic |
|---|---|---|
| January 06, 2025 | Egor Namakonov, Aarhus University | Extending Iris with liveness reasoning |
| February 10, 2025 | Adam Husted Kjelstrøm, Aarhus University | Efficient simulation of High-Level Quantum Software |
| February 24, 2025 | Koen Jacobs, INRIA | Gradual typing, for the love of dynamic! |
| March 03, 2025 | June Rousseau, Aarhus University | Formal verification of capability machine properties |
| March 10, 2025 | Laurits Bligaard, Aarhus University | Implementing the transitive closure of a step-indexed logical relation |
| March 24, 2025 | Sergei Stepanenko, Aarhus University | Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It |
| March 31, 2025 | Lasse Letager Hansen, Aarhus University | Proving the core security theorem for the TLS-1.3 Key Schedule |
| April 7, 2025 | Lasse Møldrup, Aarhus University | |
| April 14, 2025 | Adam Husted Kjelstrøm, Aarhus University | |
| April 21, 2025 | Daniel Gratzer, Aarhus University | |
| April 28, 2025 | Philipp Haselwarter, Aarhus University |