LogSem Seminar, Autumn 2021
A seminar series on program verification, logic, semantics, type theory, proof assistants and related topics.
The presentation format is pretty open. Everyone is welcome to present previous/current work,
explain interesting papers, give tutorial talks on topics you find worth sharing.
Typically, it’s 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 or virtual on Zoom.
This meeting is organized by Alejandro Aguirre.
A preliminary schedule is available below.
|March 1, 2021||Martin Bidlingmaier||The multiverse model of dependent type theory|
|March 8, 2021||Cancelled|
|March 15, 2021||Magnus Baunsgaard Kristensen||A model of Clocked Cubical Type Theory|
|March 22, 2021||Philip G. Haselwater||SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq|
|March 29, 2021||No seminar - Easter break|
|April 5, 2021||No seminar - Easter Monday|
|April 12, 2021||Cancelled|
|April 19, 2021||Neel Krishnaswami||Adjoint Reactive GUI Programming|
|April 26, 2021||Steffan Sølvsten Jørgensen||Efficient Binary Decision Diagram Manipulation in External Memory|
|May 3, 2021||Simon Wimmer||Certification of timed systems model checking: past, now, and future|
|May 10, 2021||Guilhem JABER||Complete compositional relational reasoning for state and control|
|May 17, 2021||Cancelled|
|May 24, 2021||No seminar - public holiday|
|May 31, 2021||Dan Frumin||Semantic approach to cut elimination|
|June 7, 2021||Alejandro Aguirre||Relational logics for probabilistic programs|
|June 14, 2021||Nikolaj Sidorenco||Formal security analysis of MPC-in-the-head zero-knowledge protocols|
|June 21, 2021||Cristina Matache||Recursion and sequentiality in categories of sheaves|
|September 10, 2021||Troels Henriksen||Making pigs fly: design and implementation of the Futhark language|
|September 13, 2021||Cancelled|
|September 20, 2021||Maxime Legoupil||Categorical models for focused lambda-calculus|
|September 27, 2021||Cancelled|
|October 4, 2021||Alban Reynaud||A parametrized bisimulation for interaction trees|
|October 11, 2021||Cancelled|
|October 18, 2021||No seminar - Autumn break|
|October 25, 2021||Boel Nelson||On the accuracy of differentially private algorithms|
|November 1, 2021||Jon Sterling||Between abstraction and composition|
|November 8, 2021||Pierre Cagne||Consequences of univalence on the symmetries of the spheres|
|November 15, 2021||Jean Pichon-Pharabod||Trying to make relaxed concurrency memory models more accessible: the case of Armv8|
|November 22, 2021||Jonas Kastberg Hinrichsen||Machine-Checked Semantic Session Typing|
|November 29, 2021||Patricia Johann||Deep Induction|
|December 6, 2021||No seminar|
|December 13, 2021||Aslan Askarov||Are fine-grained and coarse-grained dynamic information flow control always equally expressive?|
|December 16, 2021||Christoph Matheja||Towards a Language for Automated Verification of Probabilistic Programs|