Derek Dreyer
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
40
Venues
10
Active years
2003–2026
Best venue rank
A*
Where they publish
Papers
40 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | CPP | A Recipe for Modular Verification of Generic Tree Traversals. | Laila Elbeheiry, Michael Sammler, Robbert Krebbers, Derek Dreyer, Deepak Garg |
| 2022 | PLDI | Compass: strong and compositional library specifications in relaxed memory separation logic. | Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, Derek Dreyer |
| 2022 | PLDI | RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. | Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, Derek Dreyer |
| 2022 | PLDI | Islaris: verification of machine code against authoritative ISA semantics. | Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell |
| 2021 | PLDI | RefinedC: automating the foundational verification of C code with refined ownership types. | Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg |
| 2021 | PLDI | Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. | Simon Spies, Lennard Gher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal |
| 2020 | CAV | Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. | Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter W. O'Hearn, Jules Villard |
| 2017 | ECOOP | Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. | Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis |
| 2017 | ESOP | The Essence of Higher-Order Concurrent Separation Logic. | Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal |
| 2017 | PLDI | Repairing sequential consistency in C/C++11. | Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer |
| 2017 | POPL | A promising semantics for relaxed-memory concurrency. | Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer |
| 2016 | ICFP | Higher-order ghost state. | Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer |
| 2016 | POPL | Lightweight verification of separate compilation. | Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis |
| 2015 | ICFP | Pilsner: a compositionally verified compiler for a higher-order imperative language. | Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis |
| 2015 | PLDI | Verifying read-copy-update in a logic for weak memory. | Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis |
| 2015 | POPL | 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 |
| 2014 | OOPSLA | GPS: navigating weak memory with ghosts, protocols, and separation. | Aaron Turon, Viktor Vafeiadis, Derek Dreyer |
| 2014 | POPL | Backpack: retrofitting Haskell with interfaces. | Scott Kilpatrick, Derek Dreyer, Simon L. Peyton Jones, Simon Marlow |
| 2013 | CSL | Internalizing Relational Parametricity in the Extensional Calculus of Constructions. | Neelakantan R. Krishnaswami, Derek Dreyer |
| 2013 | ICFP | Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. | Aaron Turon, Derek Dreyer, Lars Birkedal |
| 2013 | ICFP | Mtac: a monad for typed tactic programming in Coq. | Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis |
| 2013 | POPL | The power of parameterization in coinductive proof. | Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis |
| 2013 | POPL | Logical relations for fine-grained concurrency. | Aaron Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, Derek Dreyer |
| 2012 | ICFP | Superficially substructural types. | Neelakantan R. Krishnaswami, Aaron Turon, Derek Dreyer, Deepak Garg |
| 2012 | POPL | The marriage of bisimulations and Kripke logical relations. | Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis |
| 2011 | ICFP | How to make ad hoc proof automation less ad hoc. | Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer |
| 2011 | LICS | Separation Logic in the Presence of Garbage Collection. | Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis |
| 2011 | POPL | A kripke logical relation between ML and assembly. | Chung-Kil Hur, Derek Dreyer |
| 2010 | ICFP | The impact of higher-order state and control effects on local relational reasoning. | Derek Dreyer, Georg Neis, Lars Birkedal |
| 2010 | POPL | A relational modal logic for higher-order stateful ADTs. | Derek Dreyer, Georg Neis, Andreas Rossberg, Lars Birkedal |
| 2009 | ICFP | Non-parametric parametricity. | Georg Neis, Derek Dreyer, Andreas Rossberg |
| 2009 | LICS | Logical Step-Indexed Logical Relations. | Derek Dreyer, Amal Ahmed, Lars Birkedal |
| 2009 | POPL | State-dependent representation independence. | Amal Ahmed, Derek Dreyer, Andreas Rossberg |
| 2008 | ICFP | Mixin' up the ML module system. | Derek Dreyer, Andreas Rossberg |
| 2007 | ESOP | Principal Type Schemes for Modular Programs. | Derek Dreyer, Matthias Blume |
| 2007 | ICFP | A type system for recursive modules. | Derek Dreyer |
| 2007 | POPL | Modular type classes. | Derek Dreyer, Robert Harper, Manuel M. T. Chakravarty, Gabriele Keller |
| 2005 | ICFP | Recursive type generativity. | Derek Dreyer |
| 2004 | POPL | A type system for well-founded recursion. | Derek Dreyer |
| 2003 | POPL | A type system for higher-order modules. | Derek Dreyer, Karl Crary, Robert Harper |