LogSem Seminar talks in 2025

06-01-2025: Extending Iris with liveness reasoning

Speaker: Egor Namakonov, Aarhus University

Time: 13:00-14:00

Location: Nygaard-297

Abstract: Higher-order program logics like Iris have proven extremely expressive for the verification of safety properties. However, the same level of expressivity for liveness verification is yet to be achieved. The existing work in this area had to compromise either on higher-order reasoning, compositionality, verifying the whole development foundationally, or being language-agnostic. In this talk, I’ll give an overview of a few Iris developments that deal with liveness verification. Then, I’ll introduce Lawyer - our ongoing project aiming at achieving all of the aforementioned goals - and show how to use it to verify the termination of a simple concurrent program.

10-02-2025: Efficient simulation of High-Level Quantum Software

Speaker: Adam Husted Kjelstrøm, Aarhus University

Time: 13:00-15:00

Location: Ada-333

Abstract: Simulation is a natural way to investigate program behavior. Interestingly for the quantum setting, a single simulation is enough to determine equivalence between programs, making simulation algorithms powerful tools for verifying program correctness. Practical quantum computing is hampered by the high error rates of instructions. To improve practical performance, code minimizers are employed. In this setting, Simulators can be paired with heuristic search to equivalence check candidate smaller programs. To build such code minimizers, efficient simulation algorithms are crucial. In this presentation, I will introduce a simulator for high-level quantum software. Other simulators compile the user-provided code to a low-level representation before simulating, resulting in increased software size and an (exponential) blow-up in simulation time. By directly simulating high-level code, this overhead is avoided, resulting in efficient simulation of certain classes of quantum software.

It is natural to ask whether all quantum code can be efficiently simulated. Assuming SETH, I demonstrate how some quantum code can never be efficiently simulated. Specifically, access to even a single ADD instruction is enough to encode 3SAT.

24-02-2025: Gradual typing, for the love of dynamic!

Speaker: Koen Jacobs, INRIA

Time: 13:00-15:00

Location: Ada-333

Abstract: Gradual typing has long been advocated as a means to bridge the gap between static and dynamic type disciplines, enabling a range of use cases such as the gradual migration of existing dynamically typed code to more statically typed code, or making advanced static typing disciplines more accessible. To assess whether a given gradual language can effectively support these use cases, several formal properties have been proposed, amongst which the refined criteria by Siek et al.

In this talk, we start out by introducing a concrete and realistic running example to exemplify the aforementioned use-cases, with which we then present some basic ideas behind gradual typing as they are presented in the literature. Moreover, we shall use an intuitive expectation of this example to extract a novel formal criterion about the general use-cases, inspired by the literature on secure compilation.

As we shall see, the novel criterion imposes an upper bound on how quickly a cast error may occur when importing dynamically-typed code at a particular static type. Informally, if a dynamically-typed program is semantically well-behaved at a static type, importing that program into the gradual language at said type should result in a gradual program that cannot ever (under arbitrary interaction) be responsible for a cast error.

We shall demonstrate that this novel criterion is not implied by any of the existing meta-theoretical properties of gradual languages, highlighting four concrete counter-examples from the literature. Additionally, we report on a fully formalized proof in the Coq/Rocq proof assistant (using the Iris library) that this property is satisfied within an appropriate setting of a gradualized simply typed lambda calculus.