- document
-
Jung, Ralf (author), Jourdan, Jacques-Henri (author), Krebbers, R.J. (author), Dreyer, Derek (author)Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust's safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust...journal article 2018
- document
-
Krebbers, R.J. (author), Jourdan, Jacques-Henri (author), Jung, Ralf (author), Tassarotti, Joseph (author), Kaiser, Jan-Oliver (author), Timany, Amin (author), Charguéraud, Arthur (author), Dreyer, Derek (author)A number of tools have been developed for carrying out separation-logic proofs mechanically using an interactive proof assistant. One of the most advanced such tools is the Iris Proof Mode (IPM) for Coq, which offers a rich set of tactics for making separation-logic proofs look and feel like ordinary Coq proofs. However, IPM is tied to a...journal article 2018
- document
-
Jung, Ralf (author), Krebbers, R.J. (author), Jourdan, Jacques-Henri (author), Bizjak, Aleš (author), Birkedal, Lars (author), Dreyer, Derek (author)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...journal article 2018