Actris: Session Types meet Separation Logic

Actris is a framework for reasoning about message-passing concurrency using higher-order separation logic.

Actris introduces the concept of Dependent Separation Protocols, which merge the ideas of session types with the expressivity of higher-order separation logic.

Actris is built on top of Iris—a state of the art concurrent separation logic.

Publications

2024 OOPSLA, Verified Lock-Free Session Channels with Linking,: Thomas Somers and Robbert Krebbers.
2024 OOPSLA, Multris: Functional Verification of Multiparty Message Passing in Separation Logic,: Jonas Kastberg Hinrichsen, Jules Jacobs, and Robbert Krebbers.
2024 POPL, Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing,: Jules Jacobs, Jonas Kastberg Hinrichsen, and Robbert Krebbers.
2023 ICFP, Dependent Session Protocols in Separation Logic from First Principles,: Jules Jacobs, Jonas Kastberg Hinrichsen, and Robbert Krebbers.
2023 ICFP, Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols,: Léon Gondelman, Jonas Kastberg Hinrichsen, Mário Pereira, Amin Timany, and Lars Birkedal.
2022 LMCS, Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic,: Jonas Kastberg Hinrichsen, Robbert Krebbers, and Jesper Bengtson.
2021 CPP [Distinguished Paper Award], Machine-Checked Semantic Session Typing,: Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, and Jesper Bengtson.
2020 POPL, Actris: Session-Type Based Reasoning in Separation Logic,: Jonas Kastberg Hinrichsen, Robbert Krebbers, and Jesper Bengtson.