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 Lyon
May 07, 2025Kayvan Memarian, University of Cambridge
May 12, 2025Eske Nielsen, Aarhus University
May 19, 2025Virgil Marionneau, ENS Rennes; Félix Sassus-Bourda, ENS Paris-Saclay
May 26, 2025Kwing Hei Li, Aarhus University

Previous seminars