LogSem Seminar, 2022

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.

DateWhoTopic
February 21, 2022Bastien RousseauA DSL of Combinators for Vellvm
March 14, 2022Steffan SølvstenAdiar: Binary Decision Diagrams in External Memory (TACAS 22 presentation)
April 4, 2022Aina Linn GeorgesLe Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities
April 25, 2022Zongyuan LiuA Separation Logic for Communicating Virtual Machines
May 23, 2022Bastien RousseauOptimizing Relational Symbolic Execution over Cryptographic Code
May 30, 2022Cancelled
June 13, 2022Philipp StassenA Flexible Multimodal Proof Assistant
June 20, 2022Bas SpittersType theory for critical applications: cryptography and smart contracts
June 20, 2022Eske NielsenFormalising Decentralised Exchanges in Coq
June 27, 2022Rasmus Holdsbjerg-LarsenHigh-assurance synthesis of cryptographic primitives - The BLS12 pairing groups
June 27, 2022Sergei StepanenkoThe Essence of Generalised Algebraic Data Types
September 19, 2022Egor NamakonovLiveness properties under weak memory
October 10, 2022Bastien RousseauConcurrent Cerise - A Program Logic for Multi-core Capability Machine
October 17, 2022Fall break
October 24, 2022Jonas Kastberg HinrichsenModelling and verifying distributed systems
October 31, 2022Amin TimanyA Formal and Foundational Approach to Program Verification for Safety and Security
November 8, 2022Stephanie Balzer, Carnegie Mellon UniversitySession Types for Information Flow Control and a Logical Relation for Noninterference
November 14, 2022Irfansha ShaikCompact QBF encodings for planning and 2-player games
November 21, 2022Cancelled
November 28, 2022Cancelled
December 5, 2022Ben Simner, University of CambridgeRelaxed virtual memory