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 | Cancelled | |
| April 14, 2025 | Adam Husted Kjelstrøm, Aarhus University | Simulating quantum computers: the basics |
| April 22, 2025 | Daniel Gratzer, Aarhus University | On the univalence axiom |
| April 28, 2025 | Amin Timany, Aarhus University | Context-Dependent Effects in Guarded Interaction Trees |
| May 05, 2025 | Iwan Quémerais, ENS Lyon | First-order store and visibility in the π-calculus |
| May 07, 2025 | Kayvan Memarian, University of Cambridge | Pragmatic Test-oracle Specification of a Production Hypervisor |
| May 12, 2025 | Cancelled | |
| May 19, 2025 | Virgil Marionneau, ENS Rennes | A step-indexed denotational semantics of Call-by-push-value with arbitrary recursive types in the category of COFEs |
| May 26, 2025 | Kwing Hei Li, Aarhus University | Coneris: Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs |
Previous seminars