LogSem Seminar, 2023

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.

A preliminary schedule is available below.

DateWhoTopic
January 16, 2023Pieter Bos, University of TwenteDemonstration of Vercors: a Verifier of Concurrent and Distributed Software
February 6, 2023Satoshi Kura, National Institute of Informatics / University of OxfordHigher-Order Weakest Precondition Transformers via a CPS Transformation
February 20, 2023Alejandro AguirreProgram Logics for Probabilistic Programs
February 27, 2023Daniel GratzerDenotational semantics of type theory
March 6, 2023Vincent LafeychineOverview of Proost, a student-made proof assistant in Rust
March 13, 2023Dorian LesbreDefining contextual refinement for capability machines
March 20, 2023Ira Fesefeldt, RWTH AachenExpectation-Transformer Reasoning with Concurrent Separation Logic: A story about Invariants, Quantities and their Expectation
March 27, 2023Ohad Kammar, University of EdimburghSome applications of free extensions to partial evaluation, equational-proof synthesis, and normalisation-by-evaluation
April 17, 2023Jon SterlingDenotational semantics in impredicative guarded dependent type theory
May 1, 2023Pedro H. Azevedo de Amorim, Cornell UniversityA higher-order language for Markov kernels and linear operators
May 15, 2023Ugo Dal Lago, University of Bologna and INRIA Sophia AntipolisOn Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments

Previous seminars