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.

03-03-2025: Formal verification of capability machine properties

Speaker: June Rousseau

Time: 13:00-15:00

Location: Ada-020

Abstract: In this talk, I will present the two main projects of my PhD, related to verification of capability machine (CHERI) properties. In a first part, I will present our formalisation of CHERIoT, an adapted architecture CHERI for IoT devices. I will explain how our new logical relation supports the mutually distrusful compartmentalisation model of CHERioT. In a second part, I will present how we plan to verify CHERI-TrEE, an extension of CHERI for trusted execution enclaves. More specifically, I will present you one of the main challenges we encounter when formalising CHERI-TrEE in Iris.

10-03-2025: Implementing the transitive closure of a step-indexed logical relation

Speaker: Laurits Bligaard

Time: 13:00-15:00

Location: Nygaard-298

Abstract: In this talk, I will discuss the implementation details of the transitive closure of a logical relation in Coq. Step-indexed logical relations are in general difficult to prove transitive. Instead there have been various suggestions on how to construct them such that they enjoy transitivity. One such approach is to define a new relation as essentially the transitive closure of a step-indexed logical relation. Last semester, I read up on logical relations and their formalization in Coq. As an end-of-the-semester project I implemented such a transitive closure of a step-indexed logical relation defined in Iris. I will present the details and considerations I had when adapting the general transitive-closure approach to a Iris-specific relation defined in Coq.

24-03-2025: Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It

Speaker: Sergei Stepanenko

Time: 13:00-15:00

Location: Nygaard-297

Abstract: Recursive domain equations are omnipresent in the study of programming languages, particularly in semantical models for languages with higher-order functions. While existing approaches trade off expressive power to be more amedable to mechanization, certain more expressive frameworks, such as the topos of trees, have remained primarily theoretical and lack mechanized formalization.

In this talk, I will present joint work with Amin Timany on the formalization of solutions to guarded domain equations in the category of presheaves over ordinals using the Rocq proof assistant. We address the challenges posed by previous approaches, particularly in handling transfinite step-indexing and sheaves. By simplifying previous constructions from the setting of sheaves to presheaves, we implement more user-friendly framework while preserving expressivity. I will discuss key technical insights, limitations of existing mechanizations, and the refinements that enabled a usable formalization.

31-03-2025: Proving the core security theorem for the TLS-1.3 Key Schedule

Speaker: Lasse Letager Hansen

Time: 13:00-15:00

Location: Ada-020

Abstract: In this talk we will look at how to prove security properties for the TLS-1.3 Key Schedule. This work is part of a larger effort for proving correctness and security of Bertie a TLS-1.3 implementation. The protocol is implemented in Rust, and translated into SSProve, F*, and ProVerif using the Hax framework. These parts the validate different properties of the protocol. The security proof is based on an existing pen and paper proof in the State Seperating Proof (SSP) style. We will discuss how to construct such proof for a large protocol and the difficulties of formalizing it.