Two Heuristics for the Euclidean Steiner Tree Problem. - Derek R. Dreyer; Michael L. Overton (J. Glob. Optim., 1998)

A type system for higher-order modules. - Derek Dreyer; Karl Crary; Robert Harper 001 (POPL, 2003)

Typed compilation of recursive datatypes. - Joseph Vanderwaart; Derek Dreyer; Leaf Petersen; Karl Crary; Robert Harper 001; Perry Cheng (TLDI, 2003)

A type system for well-founded recursion. - Derek Dreyer (POPL, 2004)

Principal Type Schemes for Modular Programs. - Derek Dreyer; Matthias Blume (ESOP, 2007)

A type system for recursive modules. - Derek Dreyer (ICFP, 2007)

Modular type classes. - Derek Dreyer; Robert Harper 001; Manuel M. T. Chakravarty; Gabriele Keller (POPL, 2007)

Recursive type generativity. - Derek Dreyer (J. Funct. Program., 2007)

State-dependent representation independence. - Amal Ahmed 001; Derek Dreyer; Andreas Rossberg (POPL, 2009)

A relational modal logic for higher-order stateful ADTs. - Derek Dreyer; Georg Neis; Andreas Rossberg; Lars Birkedal (POPL, 2010)

Separation Logic in the Presence of Garbage Collection. - Chung-Kil Hur; Derek Dreyer; Viktor Vafeiadis (LICS, 2011)

A kripke logical relation between ML and assembly. - Chung-Kil Hur; Derek Dreyer (POPL, 2011)

Logical Step-Indexed Logical Relations - Derek Dreyer; Amal Ahmed 001; Lars Birkedal (Log. Methods Comput. Sci., 2011)

Non-parametric parametricity. - Georg Neis; Derek Dreyer; Andreas Rossberg (J. Funct. Program., 2011)

Superficially substructural types. - Neelakantan R. Krishnaswami; Aaron Turon; Derek Dreyer; Deepak Garg 001 (ICFP, 2012)

The marriage of bisimulations and Kripke logical relations. - Chung-Kil Hur; Derek Dreyer; Georg Neis; Viktor Vafeiadis (POPL, 2012)

The impact of higher-order state and control effects on local relational reasoning. - Derek Dreyer; Georg Neis; Lars Birkedal (J. Funct. Program., 2012)

Internalizing Relational Parametricity in the Extensional Calculus of Constructions. - Neelakantan R. Krishnaswami; Derek Dreyer (CSL, 2013)

Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. - Aaron Turon; Derek Dreyer; Lars Birkedal (ICFP, 2013)

The power of parameterization in coinductive proof. - Chung-Kil Hur; Georg Neis; Derek Dreyer; Viktor Vafeiadis (POPL, 2013)

Logical relations for fine-grained concurrency. - Aaron Joseph Turon; Jacob Thamsborg; Amal Ahmed 001; Lars Birkedal; Derek Dreyer (POPL, 2013)

How to make ad hoc proof automation less ad hoc. - Georges Gonthier; Beta Ziliani; Aleksandar Nanevski; Derek Dreyer (J. Funct. Program., 2013)

SIGPLAN most influential paper awards. - Derek Dreyer (ACM SIGPLAN Notices, 2013)

Principles of POPL. - Derek Dreyer; John Field; Roberto Giacobazzi; Michael Hicks 001; Suresh Jagannathan; Mooly Sagiv; Peter Sewell; Philip Wadler (ACM SIGPLAN Notices, 2013)

Mixin' Up the ML Module System. - Andreas Rossberg; Derek Dreyer (ACM Trans. Program. Lang. Syst., 2013)

GPS: navigating weak memory with ghosts, protocols, and separation. - Aaron Turon; Viktor Vafeiadis; Derek Dreyer (OOPSLA, 2014)

Backpack: retrofitting Haskell with interfaces. - Scott Kilpatrick; Derek Dreyer; Simon L. Peyton Jones; Simon Marlow (POPL, 2014)

F-ing modules. - Andreas Rossberg; Claudio V. Russo; Derek Dreyer (J. Funct. Program., 2014)

SIGPLAN awards. - Derek Dreyer (ACM SIGPLAN Notices, 2014)

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 (ICFP, 2015)

Verifying read-copy-update in a logic for weak memory. - Joseph Tassarotti; Derek Dreyer; Viktor Vafeiadis (PLDI, 2015)

Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. - Ralf Jung 002; David Swasey; Filip Sieczkowski; Kasper Svendsen; Aaron Turon; Lars Birkedal; Derek Dreyer (POPL, 2015)

Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191). - Lars Birkedal; Derek Dreyer; Philippa Gardner; Zhong Shao 001 (Dagstuhl Reports, 2015)

Mtac: A monad for typed tactic programming in Coq. - Beta Ziliani; Derek Dreyer; Neelakantan R. Krishnaswami; Aleksandar Nanevski; Viktor Vafeiadis (J. Funct. Program., 2015)

Higher-order ghost state. - Ralf Jung 002; Robbert Krebbers; Lars Birkedal; Derek Dreyer (ICFP, 2016)

Lightweight verification of separate compilation. - Jeehoon Kang; Yoonseung Kim; Chung-Kil Hur; Derek Dreyer; Viktor Vafeiadis (POPL, 2016)

Special issue dedicated to ICFP 2014: Editorial. - Derek Dreyer; Mary Sheeran (J. Funct. Program., 2016)

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. - Jan-Oliver Kaiser; Hoang-Hai Dang; Derek Dreyer; Ori Lahav 001; Viktor Vafeiadis (ECOOP, 2017)

The Essence of Higher-Order Concurrent Separation Logic. - Robbert Krebbers; Ralf Jung 002; Ales Bizjak; Jacques-Henri Jourdan; Derek Dreyer; Lars Birkedal (ESOP, 2017)

Repairing sequential consistency in C/C++11. - Ori Lahav 001; Viktor Vafeiadis; Jeehoon Kang; Chung-Kil Hur; Derek Dreyer (PLDI, 2017)

A promising semantics for relaxed-memory concurrency. - Jeehoon Kang; Chung-Kil Hur; Ori Lahav 001; Viktor Vafeiadis; Derek Dreyer (POPL, 2017)

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact). - Jan-Oliver Kaiser; Hoang-Hai Dang; Derek Dreyer; Ori Lahav 001; Viktor Vafeiadis (Dagstuhl Artifacts Ser., 2017)

Robust and compositional verification of object capability patterns. - David Swasey; Deepak Garg 001; Derek Dreyer (Proc. ACM Program. Lang., 2017)

Iris from the ground up: A modular foundation for higher-order concurrent separation logic. - Ralf Jung 002; Robbert Krebbers; Jacques-Henri Jourdan; Ales Bizjak; Lars Birkedal; Derek Dreyer (J. Funct. Program., 2018)

RustBelt: securing the foundations of the rust programming language. - Ralf Jung 002; Jacques-Henri Jourdan; Robbert Krebbers; Derek Dreyer (Proc. ACM Program. Lang., 2018)

Mtac2: typed tactics for backward reasoning in Coq. - Jan-Oliver Kaiser; Beta Ziliani; Robbert Krebbers; Yann Régis-Gianas; Derek Dreyer (Proc. ACM Program. Lang., 2018)

MoSeL: a general, extensible modal framework for interactive proofs in separation logic. - Robbert Krebbers; Jacques-Henri Jourdan; Ralf Jung 002; Joseph Tassarotti; Jan-Oliver Kaiser; Amin Timany; Arthur Charguéraud; Derek Dreyer (Proc. ACM Program. Lang., 2018)

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 (CAV (2), 2020)

RustBelt meets relaxed memory. - Hoang-Hai Dang; Jacques-Henri Jourdan; Jan-Oliver Kaiser; Derek Dreyer (Proc. ACM Program. Lang., 2020)

Stacked borrows: an aliasing model for Rust. - Ralf Jung 002; Hoang-Hai Dang; Jeehoon Kang; Derek Dreyer (Proc. ACM Program. Lang., 2020)

The future is ours: prophecy variables in separation logic. - Ralf Jung 002; Rodolphe Lepigre; Gaurav Parthasarathy; Marianna Rapoport; Amin Timany; Derek Dreyer; Bart Jacobs 002 (Proc. ACM Program. Lang., 2020)

The high-level benefits of low-level sandboxing. - Michael Sammler; Deepak Garg 001; Derek Dreyer; Tadeusz Litak (Proc. ACM Program. Lang., 2020)

RefinedC: automating the foundational verification of C code with refined ownership types. - Michael Sammler; Rodolphe Lepigre; Robbert Krebbers; Kayvan Memarian; Derek Dreyer; Deepak Garg 001 (PLDI, 2021)

Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. - Simon Spies; Lennard Gäher; Daniel Gratzer; Joseph Tassarotti; Robbert Krebbers; Derek Dreyer; Lars Birkedal (PLDI, 2021)

Safe systems programming in Rust. - Ralf Jung 002; Jacques-Henri Jourdan; Robbert Krebbers; Derek Dreyer (Commun. ACM, 2021)

Transfinite step-indexing for termination. - Simon Spies; Neel Krishnaswami; Derek Dreyer (Proc. ACM Program. Lang., 2021)

GhostCell: separating permissions from data in Rust. - Joshua Yanovski; Hoang-Hai Dang; Ralf Jung 002; Derek Dreyer (Proc. ACM Program. Lang., 2021)

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 (PLDI, 2022)

RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. - Yusuke Matsushita 002; Xavier Denis; Jacques-Henri Jourdan; Derek Dreyer (PLDI, 2022)

Islaris: verification of machine code against authoritative ISA semantics. - Michael Sammler; Angus Hammond; Rodolphe Lepigre; Brian Campbell 001; Jean Pichon-Pharabod; Derek Dreyer; Deepak Garg 001; Peter Sewell (PLDI, 2022)

On being a PhD student of Robert Harper. - Derek Dreyer; Benjamin C. Pierce (J. Funct. Program., 2022)

Proving hypersafety compositionally. - Emanuele D'Osualdo; Azadeh Farzan; Derek Dreyer (Proc. ACM Program. Lang., 2022)

Simuliris: a separation logic framework for verifying concurrent program optimizations. - Lennard Gäher; Michael Sammler; Simon Spies; Ralf Jung 002; Hoang-Hai Dang; Robbert Krebbers; Jeehoon Kang; Derek Dreyer (Proc. ACM Program. Lang., 2022)

Finding real bugs in big programs with incorrectness logic. - Quang Loc Le; Azalea Raad; Jules Villard; Josh Berdine; Derek Dreyer; Peter W. O'Hearn (Proc. ACM Program. Lang., 2022)

VIP: verifying real-world C idioms with integer-pointer casts. - Rodolphe Lepigre; Michael Sammler; Kayvan Memarian; Robbert Krebbers; Derek Dreyer; Peter Sewell (Proc. ACM Program. Lang., 2022)

Concurrent incorrectness separation logic. - Azalea Raad; Josh Berdine; Derek Dreyer; Peter W. O'Hearn (Proc. ACM Program. Lang., 2022)

Later credits: resourceful reasoning for the later modality. - Simon Spies; Lennard Gäher; Joseph Tassarotti; Ralf Jung 002; Robbert Krebbers; Lars Birkedal; Derek Dreyer (Proc. ACM Program. Lang., 2022)

BFF: foundational and automated verification of bitfield-manipulating programs. - Fengmin Zhu; Michael Sammler; Rodolphe Lepigre; Derek Dreyer; Deepak Garg 001 (Proc. ACM Program. Lang., 2022)

DimSum: A Decentralized Approach to Multi-language Semantics and Verification. - Michael Sammler; Simon Spies; Youngju Song; Emanuele D'Osualdo; Robbert Krebbers; Deepak Garg 001; Derek Dreyer (Proc. ACM Program. Lang., 2023)

Conditional Contextual Refinement. - Youngju Song; Minki Cho; Dongjae Lee; Chung-Kil Hur; Michael Sammler; Derek Dreyer (Proc. ACM Program. Lang., 2023)

Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning. - Noam Zilberstein; Derek Dreyer; Alexandra Silva 001 (Proc. ACM Program. Lang., 2023)

Stuttering for Free. - Minki Cho; Youngju Song; Dongjae Lee; Lennard Gäher; Derek Dreyer (Proc. ACM Program. Lang., 2023)

Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. - Armaël Guéneau; Johannes Hostert; Simon Spies; Michael Sammler; Lars Birkedal; Derek Dreyer (Proc. ACM Program. Lang., 2023)

RefinedRust: A Type System for High-Assurance Verification of Rust Programs. - Lennard Gäher; Michael Sammler; Ralf Jung 002; Robbert Krebbers; Derek Dreyer (Proc. ACM Program. Lang., 2024)

Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq. - Simon Spies; Lennard Gäher; Michael Sammler; Derek Dreyer (Proc. ACM Program. Lang., 2024)

A Logical Approach to Type Soundness. - Amin Timany; Robbert Krebbers; Derek Dreyer; Lars Birkedal (J. ACM, 2024)

RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers. - Kimaya Bedarkar; Laila Elbeheiry; Michael Sammler; Lennard Gäher; Björn B. Brandenburg; Derek Dreyer; Deepak Garg 001 (Proc. ACM Program. Lang., 2025)

Data Race Freedom à la Mode. - Aïna Linn Georges; Benjamin Peters; Laila Elbeheiry; Leo White; Stephen Dolan; Richard A. Eisenberg; Chris Casinghino; François Pottier; Derek Dreyer (Proc. ACM Program. Lang., 2025)

Destabilizing Iris. - Simon Spies; Niklas Mück; Haoyi Zeng; Michael Sammler; Andrea Lattuada 001; Peter Müller 001; Derek Dreyer (Proc. ACM Program. Lang., 2025)

Tree Borrows. - Neven Villani; Johannes Hostert; Derek Dreyer; Ralf Jung 002 (Proc. ACM Program. Lang., 2025)