LogSem Seminar, Spring 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 12:00 to 14:00.
Currently all meetings are virtual on Zoom.
This meeting is organized by Danil Annenkov.
A preliminary schedule is available below.
| Date | Who | Topic |
|---|
| 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 |
Previous seminars