Number of items: 34.
Conference or Workshop Item (A Paper)
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.
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.
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.
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.
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.
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.
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.
Hur, Chung-Kil and Dreyer, Derek and Neis, Georg and Vafeiadis, Viktor
(2012)
The marriage of bisimulations and Kripke logical relations.
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.
Article
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.
Swasey, David and Garg, Deepak and Dreyer, Derek
(2017)
Robust and compositional verification of object capability patterns.
OOPSLA, 1.
89:1–89:26.
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.
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.
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.
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.
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.
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.
Neis, Georg and Dreyer, Derek and Rossberg, Andreas
(2011)
Non-parametric parametricity.
J. Funct. Program., 21 (4-5).
497–562.
This list was generated on Tue Dec 3 18:26:07 2024 CET.