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.

DateWhoTopic
January 06, 2025Egor Namakonov, Aarhus UniversityExtending Iris with liveness reasoning
February 10, 2025Adam Husted Kjelstrøm, Aarhus UniversityEfficient simulation of High-Level Quantum Software
February 24, 2025Koen Jacobs, INRIAGradual typing, for the love of dynamic!
March 03, 2025June Rousseau, Aarhus UniversityFormal verification of capability machine properties
March 10, 2025Laurits Bligaard, Aarhus UniversityImplementing the transitive closure of a step-indexed logical relation
March 24, 2025Sergei Stepanenko, Aarhus UniversitySolving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It
March 31, 2025Lasse Letager Hansen, Aarhus UniversityProving the core security theorem for the TLS-1.3 Key Schedule
April 7, 2025Cancelled
April 14, 2025Adam Husted Kjelstrøm, Aarhus UniversitySimulating quantum computers: the basics
April 22, 2025Daniel Gratzer, Aarhus UniversityOn the univalence axiom
April 28, 2025Amin Timany, Aarhus UniversityContext-Dependent Effects in Guarded Interaction Trees
May 05, 2025Iwan Quémerais, ENS LyonFirst-order store and visibility in the π-calculus
May 07, 2025Kayvan Memarian, University of CambridgePragmatic Test-oracle Specification of a Production Hypervisor
May 12, 2025Cancelled
May 19, 2025Virgil Marionneau, ENS RennesA step-indexed denotational semantics of Call-by-push-value with arbitrary recursive types in the category of COFEs
May 26, 2025Kwing Hei Li, Aarhus UniversityConeris: Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
May 26, 2025Maxime Legoupil, Aarhus UniversityIris-Wasm: formally establishing a robust and modular program logic for WebAssembly and its proposed extensions
May 26, 2025Egor Namakonov, Aarhus UniversityLawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic
June 2, 2025Lasse Møldrup, Aarhus UniversityAWDIT: An Optimal Weak Database Isolation Tester
June 30, 2025Félix SASSUS BOURDA, ENS Paris-SaclayAdding new distributions to the Eris program logic

Previous seminars