---
title: Publications
slug: Publications
---
2018
-
Reconciling High-Level Optimizations and Low-Level Code in LLVM
Juneyoung Lee, Chung-Kil Hur, Ralf Jung, Zhengyang Liu, John Regehr, Nuno P. Lopes
In OOPSLA 2018
[paper] [paper website]
-
MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
In ICFP 2018
[paper] [paper 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
[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
[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
[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]