Number of items: 34.
Jung, Ralf and Jourdan, Jacques-Henri and Krebbers, Robbert and Dreyer, Derek
(2018)
RustBelt: securing the foundations of the rust programming language.
PACMPL, 2 (POPL).
66:1–66:34.
Kang, Jeehoon and Hur, Chung-Kil and Lahav, Ori and Vafeiadis, Viktor and Dreyer, Derek
(2017)
A promising semantics for relaxed-memory concurrency.
Krebbers, Robbert and Jung, Ralf and Bizjak, Ales and Jourdan, Jacques-Henri and Dreyer, Derek and Birkedal, Lars
(2017)
The Essence of Higher-Order Concurrent Separation Logic.
Lahav, Ori and Vafeiadis, Viktor and Kang, Jeehoon and Hur, Chung-Kil and Dreyer, Derek
(2017)
Repairing sequential consistency in C/C++11.
Lahav, Ori and Vafeiadis, Viktor and Kang, Jeehoon and Hur, Chung-Kil and Dreyer, Derek
(2017)
Repairing sequential consistency in C/C++11.
Swasey, David and Garg, Deepak and Dreyer, Derek
(2017)
Robust and compositional verification of object capability patterns.
OOPSLA, 1.
89:1–89:26.
Kaiser, Jan-Oliver and Dang, Hoang-Hai and Dreyer, Derek and Lahav, Ori and Vafeiadis, Viktor
(2017)
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris.
Kang, Jeehoon and Kim, Yoonseung and Hur, Chung-Kil and Dreyer, Derek and Vafeiadis, Viktor
(2016)
Lightweight verification of separate compilation.
Jung, Ralf and Krebbers, Robbert and Birkedal, Lars and Dreyer, Derek
(2016)
Higher-order ghost state.
Dreyer, Derek and Sheeran, Mary
(2016)
Special issue dedicated to ICFP 2014: Editorial.
J. Funct. Program., 26.
e20.
Birkedal, Lars and Dreyer, Derek and Gardner, Philippa and Shao, Zhong
(2015)
Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191).
Dagstuhl Reports, 5 (5).
pp. 1-23.
Jung, Ralf and Swasey, David and Sieczkowski, Filip and Svendsen, Kasper and Turon, Aaron and Birkedal, Lars and Dreyer, Derek
(2015)
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning.
Ziliani, Beta and Dreyer, Derek and Krishnaswami, Neelakantan R. and Nanevski, Aleksandar and Vafeiadis, Viktor
(2015)
Mtac: A monad for typed tactic programming in Coq.
J. Funct. Program., 25.
Neis, Georg and Hur, Chung-Kil and Kaiser, Jan-Oliver and McLaughlin, Craig and Dreyer, Derek and Vafeiadis, Viktor
(2015)
Pilsner: a compositionally verified compiler for a higher-order imperative language.
Tassarotti, Joseph and Dreyer, Derek and Vafeiadis, Viktor
(2015)
Verifying read-copy-update in a logic for weak memory.
Birkedal, Lars and Dreyer, Derek and Gardner, Philippa and Shao, Zhong
(2015)
Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191).
Dagstuhl Reports, 5 (5).
1–23.
Rossberg, Andreas and Russo, Claudio V and Dreyer, Derek
(2014)
F-ing modules.
J. Funct. Program., 24 (5).
pp. 529-607.
Turon, Aaron and Vafeiadis, Viktor and Dreyer, Derek
(2014)
GPS: navigating weak memory with ghosts, protocols, and separation.
Kilpatrick, Scott and Dreyer, Derek and Jones, Simon L. Peyton and Marlow, Simon
(2014)
Backpack: retrofitting Haskell with interfaces.
Gonthier, Georges and Ziliani, Beta and Nanevski, Aleksandar and Dreyer, Derek
(2013)
How to make ad hoc proof automation less ad hoc.
J. Funct. Program., 23 (4).
pp. 357-401.
Ziliani, Beta and Dreyer, Derek and Krishnaswami, Neelakantan R. and Nanevski, Aleksandar and Vafeiadis, Viktor
(2013)
Mtac: a monad for typed tactic programming in Coq.
Krishnaswami, Neelakantan R. and Dreyer, Derek
(2013)
Internalizing Relational Parametricity in the Extensional Calculus of Constructions.
Turon, Aaron and Thamsborg, Jacob and Ahmed, Amal and Birkedal, Lars and Dreyer, Derek
(2013)
Logical relations for fine-grained concurrency.
Rossberg, Andreas and Dreyer, Derek
(2013)
Mixin' Up the ML Module System.
ACM Trans. Program. Lang. Syst., 35 (1).
2:1–2:84.
Rossberg, Andreas and Dreyer, Derek
(2013)
Mixin' Up the ML Module System.
ACM Trans. Program. Lang. Syst., 35 (1).
2:1–2:84.
Turon, Aaron and Dreyer, Derek and Birkedal, Lars
(2013)
Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency.
Hur, Chung-Kil and Neis, Georg and Dreyer, Derek and Vafeiadis, Viktor
(2013)
The power of parameterization in coinductive proof.
Krishnaswami, Neelakantan R. and Turon, Aaron and Dreyer, Derek and Garg, Deepak
(2012)
Superficially substructural types.
Dreyer, Derek and Neis, Georg and Birkedal, Lars
(2012)
The impact of higher-order state and control effects on local relational reasoning.
J. Funct. Program., 22 (4-5).
477–528.
Hur, Chung-Kil and Dreyer, Derek and Neis, Georg and Vafeiadis, Viktor
(2012)
The marriage of bisimulations and Kripke logical relations.
Neis, Georg and Dreyer, Derek and Rossberg, Andreas
(2011)
Non-parametric parametricity.
J. Funct. Program., 21 (4-5).
497–562.
Hur, Chung-Kil and Dreyer, Derek and Vafeiadis, Viktor
(2011)
Separation Logic in the Presence of Garbage Collection.
Hur, Chung-Kil and Dreyer, Derek
(2011)
A kripke logical relation between ML and assembly.
Dreyer, Derek and Neis, Georg and Rossberg, Andreas and Birkedal, Lars
(2010)
A relational modal logic for higher-order stateful ADTs.
This list was generated on Tue Dec 3 18:26:07 2024 CET.