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.

DateWhoTopic
March 1, 2021Martin BidlingmaierThe multiverse model of dependent type theory
March 8, 2021Cancelled
March 15, 2021Magnus Baunsgaard KristensenA model of Clocked Cubical Type Theory
March 22, 2021Philip G. HaselwaterSSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
March 29, 2021No seminar - Easter break
April 5, 2021No seminar - Easter Monday
April 12, 2021Cancelled
April 19, 2021Neel KrishnaswamiAdjoint Reactive GUI Programming
April 26, 2021Steffan Sølvsten JørgensenEfficient Binary Decision Diagram Manipulation in External Memory
May 3, 2021Simon WimmerCertification of timed systems model checking: past, now, and future
May 10, 2021Guilhem JABERComplete compositional relational reasoning for state and control
May 17, 2021Cancelled
May 24, 2021No seminar - public holiday
May 31, 2021Dan FruminSemantic approach to cut elimination
June 7, 2021Alejandro AguirreRelational logics for probabilistic programs
June 14, 2021Nikolaj SidorencoFormal security analysis of MPC-in-the-head zero-knowledge protocols
June 21, 2021Cristina MatacheRecursion and sequentiality in categories of sheaves

Previous seminars