Separation Logic And Beyond

Can you tell us a little bit about yourself and your research field?

My name is Lars Birkedal, and I’m a professor at Aarhus University, where I lead the Center for Basic Research in Program Verification and the Logic and Semantics Group. My research field is program verification, and I also do quite a bit of work on type theory, specifically on guarded type theory.

You were recently awarded the Alonzo Church Award for Outstanding Contributions to Logic and Computation, specifically for your work on the design and implementation of Iris, a higher-order concurrent separation logic framework. What is the story behind Iris?

When I was finishing up my PhD at CMU in 1999, I was lucky enough to learn about the beginnings of separation logic from John Reynolds. After I moved back to Denmark, one of my first research projects was together with John—we used separation logic to verify the correctness of a copying garbage collector. In my group, later on, we made several contributions to sequential separation logic. In particular, we were some of the first to move the study of separation logic from focusing on low-level C-like languages to languages with linguistic facilities for modular programming such as higher order functions and objects. In order to achieve this, we developed a new method for establishing soundness of separation logic by so-called “baking-in” the frame rule into the interpretation of Hoare triples. In the original work, the soundness of the frame rule relied on some subtle properties of the operational semantics, which are quite difficult to prove for languages that also have higher order functions. Afterwards, we also introduced higher order frame rules, and we showed how to model higher order separation logic. In hindsight, this was perhaps quite simple, but at the time it was complicated by the fact that many of the programming languages people studied were for languages with mutable stack variables.

We also came up with another simple idea called “nested triples”, which means that you can use Hoare triples in your pre- and post-conditions to specify higher order functions. Later on, we worked on concurrent separation logic where, in particular, we introduced a logic called ICAP—Impredicative Concurrent Abstract Predicates—which for the first time made it possible to model so-called impredicative invariants. The latter are invariants that contain any predicate from the logic. The key point in this development was the semantics used to show the soundness of this logic. Here we made use of some of our work on guarded type theory. Concretely, it involved modeling the space of propositions of the logic using a solution to a guarded recursive domain equation. And then we also worked a bit on Views, together with collaborators from the UK. This was a first step towards a more unified general framework for concurrent separation logic. Iris resulted from building on this line of work on higher order concurrent separation logic, in combination with another line of work that I’ve done in collaboration with Derek Dreyer, on logical relations for higher order, imperative and concurrent programming languages.

Another important ingredient was added by my then postdoc Robbert Krebbers, who improved on an earlier formalization we had on solutions to recursive domain equations made by my student Filip Sieczkowski. Robbert also came up with a very important proof mode for Iris, which allows you to do formal proofs in Iris in much the same way as you do it in Coq.

Since then, we’ve explored the use of Iris to a wide range of programming languages and programs, and also a wider range of properties, ranging from functional correctness to robust safety for capability machines, and to relational models for non-interference and other projects. This has been made possible in part by a generous grant from the Villum Foundation here in Denmark.

How do you see this research area developing in the future?

I think there are many interesting directions, some of which we’re going to investigate in the ERC grant that I have recently received. It is called CHORDS (Compositional Higher Order Reasoning about Distributed Systems), and the aim is basically to explore the use of extensions of Iris to reasoning about distributed systems.

Broadly speaking, we’ll focus on three topics. One is on safety properties of distributed systems. For example, implementations of distributed key-value stores or distributed transactions. Another focus is on liveness properties, and the third one is security properties. The latter one will involve some reasoning about probabilistic program properties.

Could you provide us with a preview of your invited talk at ETAPS 2024?

As I alluded to earlier, one of the cool things with Iris is that you can also use it to develop relational higher order separation logics. These have been quite useful for reasoning about relational problems such as contextual refinement and non-interference, formalized in Iris and Coq. In the talk, I’ll try to present some of our recent work on extending this approach to probabilistic higher order programs. I will introduce two new probabilistic relational logics called Clutch and Caliper, which can be used to reason about contextual refinement and almost-sure termination for probabilistic higher-order programs. In particular, I’ll try to emphasize how one can make use of some ideas from separation logic to make the reasoning simpler and go beyond what one could do with earlier proposals. The way we’re thinking of this in the context of the ERC project is that these are the first steps of how to extend some of our techniques to probabilistic languages.

How easy is it for you to pique the interest of young students in this research field? Additionally, what advice would you offer someone who is just beginning in this area?

I don’t think it has ever been easy to attract people to work in this field. The young students have very many good and interesting opportunities. We have been lucky to attract students from around the world, and in the group we do our best to help them get a good start, and we try to foster a collaborative and supportive research environment.

I don’t think that there is just one piece of advice we give young students, this all depends on the individuals' background etc. I guess one thing we try to emphasize is that one shouldn’t be afraid of trying to address some difficult case studies and to learn something new in that process. I think one thing we’ve managed to do in my group is to explore a number of different new directions; we hope in that process that we can learn something new and contribute a bit to the field.

To what extent do you collaborate with industry as part of your ERC grant?

Some of our sub-projects have some interest from the industry. We have been using Iris for verifying properties of the so-called capability systems, which are a new kind of hardware systems. That has a lot of interest from Arm, for example, who has ongoing collaborations with the CHERI group in Cambridge. One can say that the group in Cambridge is a bit more on the practical end of the capability research work—e.g., they explore how to use capabilities for practical operating systems. We are trying to develop some of the theory, which allows one to prove that capabilities can enforce certain security guarantees. We also try to use Iris for verifying some other low-level systems like hypervisors. Some of this work has been done in a project together with several other international groups, and that’s been supported by Google. I have also received a faculty award from Amazon; they have supported our work on distributed systems.

Whom would you like to see interviewed on the ETAPS blog in the future?

There are many good candidates; I think that Amal Ahmed and Stephanie Weirich, for instance, would be good candidates.