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.
|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|