---
title: Publications
slug: Publications
---
Under Submission
-
RustBelt: Securing the Foundations of the Rust Programming Language
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
[preprint] [project website (incl. appendix and Coq formalization)]
-
Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, Derek Dreyer
[preprint] [project website (incl. appendix and Coq formalization)]
2017
-
The Essence of Higher-Order Concurrent Separation Logic
Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal
In ESOP 2017: 26th European Symposium on Programming
[paper] [project website (incl. appendix and Coq formalization)]
-
A Higher-Order Logic for Concurrent Termination-Preserving Refinement
Joseph Tassarotti, Ralf Jung, Robert Harper
In ESOP 2017: 26th European Symposium on Programming
[paper] [paper website (incl. Coq formalization)]
2016
2015
-
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer
In POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
[paper] [project website (incl. appendix and Coq formalization)] [talk (slides)]
2013
-
An Intermediate Language To Formally Justify Memory Access Reordering (Bachelor's Thesis)
Ralf Jung, Supervisor: Sebastian Hack, Advisor: Sigurd Schneider
[pdf] [slides] [coq]