LogSem Seminar, 2024

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
September 30, 2024Sergei Stepanenko, Aarhus UniversityIntroduction to Guarded Interaction Trees
October 07, 2024Arnaud Daby-Seesaram, Aarhus UniversityOsiris: an Iris-based program logic for OCaml
October 10, 2024Justin Hsu, Cornell UniversityType Systems for Numerical Error Analysis
October 14, 2024Maxime Robert Sébastien Legoupil, Aarhus UniversityIris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly
October 21, 2024Kwing Hei Li, Aarhus UniversityHow to deal with rejections – Separation logics for probability
October 28, 2024Armaël Guéneau, INRIAThe state of the Creusot verifier
November 04, 2024Jean Pichon-Pharabod, Aarhus UniversitySynchronous Programming for Kids: A Manifesto
November 18, 2024Amal Ahmed, Northeastern UniversityFormally Specifying ABIs using Realistic Realizability
November 25, 2024Zongyuan Liu, Aarhus UniversityReasoning about concurrency with graphs instead of heaps in Iris
December 02, 2024Steffan Christ Sølvsten, Aarhus UniversityCorrectness of Time-forward Processing Algorithms
December 09, 2024Ilya Sergey, National University of SingaporeCompositional Verification of Composite Byzantine Protocols
December 10, 2024Ilya Sergey, National University of SingaporeMechanised Hypersafety Proofs about Structured Data