Iris from the ground up: A modular foundation for higher-order concurrent separation logic
By Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, A. Bizjak, Lars Birkedal, Derek Dreyer. Journal of functional programming, 2018
465 citations recorded by the source corpus.
Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. Iris was designed with the express goal of simplifying and consolidating the foundations of modern separation logics, but it has evolved over time, and the design and semantic foundations of Iris itself have yet to be fully written down and explained together properly in one place. Here, we attempt to fill this gap, presenting a reasonably complete picture of the latest version of Iris (version 3.1), from first principles and in one coherent narrative.
Subfields: Artificial Intelligence, Computer Networks and Communications
View Paper: https://www.semanticscholar.org/paper/0a40611a839d7e399a6647418984e60790e6910a
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
In Computer Networks and Communications
Citations in the corpus
- RustBelt: securing the foundations of the rust programming language (2017, methodology): “…Krebbers et al. 2017a], which in the past year has been equipped with tactical support for conducting machine-checked proofs of programs in Coq [Krebbers et al. 2017b] and deployed in several ongoing verification projects [Kaiser et al. 2017; Swasey et al. 2017; Tassarotti et al. 2017; Timany…”