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.
|January 16, 2023||Pieter Bos, University of Twente||Demonstration of Vercors: a Verifier of Concurrent and Distributed Software|
|February 6, 2023||Satoshi Kura, National Institute of Informatics / University of Oxford||Higher-Order Weakest Precondition Transformers via a CPS Transformation|
|February 20, 2023||Alejandro Aguirre||Program Logics for Probabilistic Programs|
|February 27, 2023||Daniel Gratzer||Denotational semantics of type theory|
|March 6, 2023||Vincent Lafeychine||Overview of Proost, a student-made proof assistant in Rust|
|March 13, 2023||Dorian Lesbre||Defining contextual refinement for capability machines|
|March 20, 2023||Ira Fesefeldt, RWTH Aachen||Expectation-Transformer Reasoning with Concurrent Separation Logic: A story about Invariants, Quantities and their Expectation|
|March 27, 2023||Ohad Kammar, University of Edimburgh||Some applications of free extensions to partial evaluation, equational-proof synthesis, and normalisation-by-evaluation|
|April 17, 2023||Jon Sterling||Denotational semantics in impredicative guarded dependent type theory|
|May 1, 2023||Pedro H. Azevedo de Amorim, Cornell University||A higher-order language for Markov kernels and linear operators|
|May 15, 2023||Ugo Dal Lago, University of Bologna and INRIA Sophia Antipolis||On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments|