Derek Dreyer

According to our database, Derek Dreyer authored at least 73 papers between 1998 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

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., October, 2023

Stuttering for Free.

Minki Cho, Youngju Song, Dongjae Lee, Lennard Gäher, Derek Dreyer

Proc. ACM Program. Lang., October, 2023

Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning.

Noam Zilberstein, Derek Dreyer, Alexandra Silva

Proc. ACM Program. Lang., April, 2023

Conditional Contextual Refinement.

Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, Derek Dreyer

Proc. ACM Program. Lang., January, 2023

DimSum: A Decentralized Approach to Multi-language Semantics and Verification.

Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, Derek Dreyer

Proc. ACM Program. Lang., January, 2023

2022

BFF: foundational and automated verification of bitfield-manipulating programs.

Fengmin Zhu, Michael Sammler, Rodolphe Lepigre, Derek Dreyer, Deepak Garg

Proc. ACM Program. Lang., 2022

Later credits: resourceful reasoning for the later modality.

Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer

Proc. ACM Program. Lang., 2022

Concurrent incorrectness separation logic.

Azalea Raad, 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

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

Simuliris: a separation logic framework for verifying concurrent program optimizations.

Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer

Proc. ACM Program. Lang., 2022

Proving hypersafety compositionally.

Emanuele D'Osualdo, Azadeh Farzan, Derek Dreyer

Proc. ACM Program. Lang., 2022

On being a PhD student of Robert Harper.

Derek Dreyer, Benjamin C. Pierce

J. Funct. Program., 2022

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

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code.

Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, Derek Dreyer

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

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

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

2021

GhostCell: separating permissions from data in Rust.

Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, Derek Dreyer

Proc. ACM Program. Lang., 2021

Transfinite step-indexing for termination.

Simon Spies, Neel Krishnaswami, Derek Dreyer

Proc. ACM Program. Lang., 2021

Safe systems programming in Rust.

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer

Commun. ACM, 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

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

RefinedC: automating the foundational verification of C code with refined ownership types.

Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

2020

The high-level benefits of low-level sandboxing.

Michael Sammler, Deepak Garg, Derek Dreyer, Tadeusz Litak

Proc. ACM Program. Lang., 2020

The future is ours: prophecy variables in separation logic.

Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs

Proc. ACM Program. Lang., 2020

Stacked borrows: an aliasing model for Rust.

Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer

Proc. ACM Program. Lang., 2020

RustBelt meets relaxed memory.

Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer

Proc. ACM Program. Lang., 2020

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

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2018

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

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

RustBelt: securing the foundations of the rust programming language.

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer

Proc. ACM Program. Lang., 2018

Iris from the ground up: A modular foundation for higher-order concurrent separation logic.

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, Derek Dreyer

J. Funct. Program., 2018

2017

Robust and compositional verification of object capability patterns.

David Swasey, Deepak Garg, Derek Dreyer

Proc. ACM Program. Lang., 2017

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact).

Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis

Dagstuhl Artifacts Ser., 2017

A promising semantics for relaxed-memory concurrency.

Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Repairing sequential consistency in C/C++11.

Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer

Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

The Essence of Higher-Order Concurrent Separation Logic.

Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal

Proceedings of the Programming Languages and Systems, 2017

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris.

Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis

Proceedings of the 31st European Conference on Object-Oriented Programming, 2017

2016

Special issue dedicated to ICFP 2014: Editorial.

Derek Dreyer, Mary Sheeran

J. Funct. Program., 2016

Lightweight verification of separate compilation.

Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Higher-order ghost state.

Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

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

Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191).

Lars Birkedal, Derek Dreyer, Philippa Gardner, Zhong Shao

Dagstuhl Reports, 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

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Verifying read-copy-update in a logic for weak memory.

Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

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

Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

2014

SIGPLAN awards.

Derek Dreyer

ACM SIGPLAN Notices, 2014

F-ing modules.

Andreas Rossberg, Claudio V. Russo, Derek Dreyer

J. Funct. Program., 2014

Backpack: retrofitting Haskell with interfaces.

Scott Kilpatrick, Derek Dreyer, Simon L. Peyton Jones, Simon Marlow

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

GPS: navigating weak memory with ghosts, protocols, and separation.

Aaron Turon, Viktor Vafeiadis, Derek Dreyer

Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, 2014

2013

Mixin' Up the ML Module System.

Andreas Rossberg, Derek Dreyer

ACM Trans. Program. Lang. Syst., 2013

Principles of POPL.

Derek Dreyer, John Field, Roberto Giacobazzi, Michael Hicks, Suresh Jagannathan, Mooly Sagiv, Peter Sewell, Philip Wadler

ACM SIGPLAN Notices, 2013

SIGPLAN most influential paper awards.

Derek Dreyer

ACM SIGPLAN Notices, 2013

How to make ad hoc proof automation less ad hoc.

Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer

J. Funct. Program., 2013

Logical relations for fine-grained concurrency.

Aaron Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, Derek Dreyer

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

The power of parameterization in coinductive proof.

Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency.

Aaron Turon, Derek Dreyer, Lars Birkedal

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

Internalizing Relational Parametricity in the Extensional Calculus of Constructions.

Neelakantan R. Krishnaswami, Derek Dreyer

Proceedings of the Computer Science Logic 2013 (CSL 2013), 2013

2012

The impact of higher-order state and control effects on local relational reasoning.

Derek Dreyer, Georg Neis, Lars Birkedal

J. Funct. Program., 2012

The marriage of bisimulations and Kripke logical relations.

Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Superficially substructural types.

Neelakantan R. Krishnaswami, Aaron Turon, Derek Dreyer, Deepak Garg

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2012

2011

Non-parametric parametricity.

Georg Neis, Derek Dreyer, Andreas Rossberg

J. Funct. Program., 2011

Logical Step-Indexed Logical Relations

Derek Dreyer, Amal Ahmed, Lars Birkedal

Log. Methods Comput. Sci., 2011

A kripke logical relation between ML and assembly.

Chung-Kil Hur, Derek Dreyer

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Separation Logic in the Presence of Garbage Collection.

Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis

Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, 2011

2010

A relational modal logic for higher-order stateful ADTs.

Derek Dreyer, Georg Neis, Andreas Rossberg, Lars Birkedal

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

2009

State-dependent representation independence.

Amal Ahmed, Derek Dreyer, Andreas Rossberg

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

2007

Recursive type generativity.

Derek Dreyer

J. Funct. Program., 2007

Modular type classes.

Derek Dreyer, Robert Harper, Manuel M. T. Chakravarty, Gabriele Keller

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

A type system for recursive modules.

Derek Dreyer

Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, 2007

Principal Type Schemes for Modular Programs.

Derek Dreyer, Matthias Blume

Proceedings of the Programming Languages and Systems, 2007

2004

A type system for well-founded recursion.

Derek Dreyer

Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2004

2003

Typed compilation of recursive datatypes.

Joseph Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, Perry Cheng

Proceedings of TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2003

A type system for higher-order modules.

Derek Dreyer, Karl Crary, Robert Harper

Proceedings of the Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2003

1998

Two Heuristics for the Euclidean Steiner Tree Problem.

Derek R. Dreyer, Michael L. Overton

J. Glob. Optim., 1998