Derek Dreyer - RankMe

93 papers A* 22A 15B 2Journal 49Unranked 3

Year	Rank	Type	Title / Venue / Authors
2026	B	`conf`	A Recipe for Modular Verification of Generic Tree Traversals. CPP Laila Elbeheiry, Michael Sammler, Robbert Krebbers, Derek Dreyer, Deepak Garg
2026	J	`jnl`	Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation. Proc. ACM Program. Lang. Niklas Mück, Aïna Linn Georges, Derek Dreyer, Deepak Garg, Michael Sammler
2025	J	`jnl`	Data Race Freedom à la Mode. Proc. ACM Program. Lang. Aïna Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White, Stephen Dolan, Richard A. Eisenberg, Chris Casinghino, François Pottier, Derek Dreyer
2025	J	`jnl`	Destabilizing Iris. Proc. ACM Program. Lang. Simon Spies, Niklas Mück, Haoyi Zeng, Michael Sammler, Andrea Lattuada, Peter Müller, Derek Dreyer
2025	J	`jnl`	RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers. Proc. ACM Program. Lang. Kimaya Bedarkar, Laila Elbeheiry, Michael Sammler, Lennard Gäher, Björn B. Brandenburg, Derek Dreyer, Deepak Garg
2025	J	`jnl`	Tree Borrows. Proc. ACM Program. Lang. Neven Villani, Johannes Hostert, Derek Dreyer, Ralf Jung
2024	J	`jnl`	A Logical Approach to Type Soundness. J. ACM Amin Timany, Robbert Krebbers, Derek Dreyer, Lars Birkedal
2024	J	`jnl`	Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq. Proc. ACM Program. Lang. Simon Spies, Lennard Gäher, Michael Sammler, Derek Dreyer
2024	J	`jnl`	RefinedRust: A Type System for High-Assurance Verification of Rust Programs. Proc. ACM Program. Lang. Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, Derek Dreyer
2023	J	`jnl`	Conditional Contextual Refinement. Proc. ACM Program. Lang. Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, Derek Dreyer
2023	J	`jnl`	DimSum: A Decentralized Approach to Multi-language Semantics and Verification. Proc. ACM Program. Lang. Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, Derek Dreyer
2023	J	`jnl`	Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. Proc. ACM Program. Lang. Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer
2023	J	`jnl`	Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning. CoRR Noam Zilberstein, Derek Dreyer, Alexandra Silva
2023	J	`jnl`	Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning. Proc. ACM Program. Lang. Noam Zilberstein, Derek Dreyer, Alexandra Silva
2023	J	`jnl`	Stuttering for Free. Proc. ACM Program. Lang. Minki Cho, Youngju Song, Dongjae Lee, Lennard Gäher, Derek Dreyer
2022	J	`jnl`	BFF: foundational and automated verification of bitfield-manipulating programs. Proc. ACM Program. Lang. Fengmin Zhu, Michael Sammler, Rodolphe Lepigre, Derek Dreyer, Deepak Garg
2022	A*	`conf`	Compass: strong and compositional library specifications in relaxed memory separation logic. PLDI Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, Derek Dreyer
2022	J	`jnl`	Concurrent incorrectness separation logic. Proc. ACM Program. Lang. Azalea Raad, Josh Berdine, Derek Dreyer, Peter W. O'Hearn
2022	J	`jnl`	Finding real bugs in big programs with incorrectness logic. Proc. ACM Program. Lang. Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, Peter W. O'Hearn
2022	A*	`conf`	Islaris: verification of machine code against authoritative ISA semantics. PLDI Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell
2022	J	`jnl`	Later credits: resourceful reasoning for the later modality. Proc. ACM Program. Lang. Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
2022	J	`jnl`	On being a PhD student of Robert Harper. J. Funct. Program. Derek Dreyer, Benjamin C. Pierce
2022	J	`jnl`	Proving Hypersafety Compositionally. CoRR Emanuele D'Osualdo, Azadeh Farzan, Derek Dreyer
2022	J	`jnl`	Proving hypersafety compositionally. Proc. ACM Program. Lang. Emanuele D'Osualdo, Azadeh Farzan, Derek Dreyer
2022	A*	`conf`	RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. PLDI Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, Derek Dreyer
2022	J	`jnl`	Simuliris: a separation logic framework for verifying concurrent program optimizations. Proc. ACM Program. Lang. Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer
2022	J	`jnl`	VIP: verifying real-world C idioms with integer-pointer casts. Proc. ACM Program. Lang. Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell
2021	J	`jnl`	GhostCell: separating permissions from data in Rust. Proc. ACM Program. Lang. Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, Derek Dreyer
2021	A*	`conf`	RefinedC: automating the foundational verification of C code with refined ownership types. PLDI Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg
2021	J	`jnl`	Safe systems programming in Rust. Commun. ACM Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
2021	A*	`conf`	Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. PLDI Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal
2021	J	`jnl`	Transfinite step-indexing for termination. Proc. ACM Program. Lang. Simon Spies, Neel Krishnaswami, Derek Dreyer
2020	—	`conf`	Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. CAV (2) Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter W. O'Hearn, Jules Villard
2020	J	`jnl`	RustBelt meets relaxed memory. Proc. ACM Program. Lang. Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer
2020	J	`jnl`	Stacked borrows: an aliasing model for Rust. Proc. ACM Program. Lang. Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer
2020	J	`jnl`	The future is ours: prophecy variables in separation logic. Proc. ACM Program. Lang. Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs
2020	J	`jnl`	The high-level benefits of low-level sandboxing. Proc. ACM Program. Lang. Michael Sammler, Deepak Garg, Derek Dreyer, Tadeusz Litak
2018	J	`jnl`	Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, Derek Dreyer
2018	J	`jnl`	MoSeL: a general, extensible modal framework for interactive proofs in separation logic. Proc. ACM Program. Lang. Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
2018	J	`jnl`	Mtac2: typed tactics for backward reasoning in Coq. Proc. ACM Program. Lang. Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer
2018	J	`jnl`	RustBelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang. Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
2017	A*	`conf`	A promising semantics for relaxed-memory concurrency. POPL Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer
2017	A*	`conf`	Repairing sequential consistency in C/C++11. PLDI Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer
2017	J	`jnl`	Robust and compositional verification of object capability patterns. Proc. ACM Program. Lang. David Swasey, Deepak Garg, Derek Dreyer
2017	J	`jnl`	Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact). Dagstuhl Artifacts Ser. Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis
2017	A	`conf`	Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. ECOOP Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis
2017	A	`conf`	The Essence of Higher-Order Concurrent Separation Logic. ESOP Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal
2016	A	`conf`	Higher-order ghost state. ICFP Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
2016	A*	`conf`	Lightweight verification of separate compilation. POPL Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis
2016	J	`jnl`	Special issue dedicated to ICFP 2014: Editorial. J. Funct. Program. Derek Dreyer, Mary Sheeran
2015	J	`jnl`	Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191). Dagstuhl Reports Lars Birkedal, Derek Dreyer, Philippa Gardner, Zhong Shao
2015	A*	`conf`	Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. POPL Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer
2015	J	`jnl`	Mtac: A monad for typed tactic programming in Coq. J. Funct. Program. Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis
2015	A	`conf`	Pilsner: a compositionally verified compiler for a higher-order imperative language. ICFP Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis
2015	A*	`conf`	Verifying read-copy-update in a logic for weak memory. PLDI Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis
2014	A*	`conf`	Backpack: retrofitting Haskell with interfaces. POPL Scott Kilpatrick, Derek Dreyer, Simon L. Peyton Jones, Simon Marlow
2014	J	`jnl`	F-ing modules. J. Funct. Program. Andreas Rossberg, Claudio V. Russo, Derek Dreyer
2014	A	`conf`	GPS: navigating weak memory with ghosts, protocols, and separation. OOPSLA Aaron Turon, Viktor Vafeiadis, Derek Dreyer
2014	J	`jnl`	SIGPLAN awards. ACM SIGPLAN Notices Derek Dreyer
2013	J	`jnl`	How to make ad hoc proof automation less ad hoc. J. Funct. Program. Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer
2013	B	`conf`	Internalizing Relational Parametricity in the Extensional Calculus of Constructions. CSL Neelakantan R. Krishnaswami, Derek Dreyer
2013	A*	`conf`	Logical relations for fine-grained concurrency. POPL Aaron Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, Derek Dreyer
2013	J	`jnl`	Mixin' Up the ML Module System. ACM Trans. Program. Lang. Syst. Andreas Rossberg, Derek Dreyer
2013	A	`conf`	Mtac: a monad for typed tactic programming in Coq. ICFP Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis
2013	J	`jnl`	Principles of POPL. ACM SIGPLAN Notices Derek Dreyer, John Field, Roberto Giacobazzi, Michael Hicks, Suresh Jagannathan, Mooly Sagiv, Peter Sewell, Philip Wadler
2013	J	`jnl`	SIGPLAN most influential paper awards. ACM SIGPLAN Notices Derek Dreyer
2013	A*	`conf`	The power of parameterization in coinductive proof. POPL Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis
2013	A	`conf`	Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. ICFP Aaron Turon, Derek Dreyer, Lars Birkedal
2012	A	`conf`	Superficially substructural types. ICFP Neelakantan R. Krishnaswami, Aaron Turon, Derek Dreyer, Deepak Garg
2012	J	`jnl`	The impact of higher-order state and control effects on local relational reasoning. J. Funct. Program. Derek Dreyer, Georg Neis, Lars Birkedal
2012	A*	`conf`	The marriage of bisimulations and Kripke logical relations. POPL Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis
2011	A*	`conf`	A kripke logical relation between ML and assembly. POPL Chung-Kil Hur, Derek Dreyer
2011	A	`conf`	How to make ad hoc proof automation less ad hoc. ICFP Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer
2011	J	`jnl`	Logical Step-Indexed Logical Relations Log. Methods Comput. Sci. Derek Dreyer, Amal Ahmed, Lars Birkedal
2011	J	`jnl`	Non-parametric parametricity. J. Funct. Program. Georg Neis, Derek Dreyer, Andreas Rossberg
2011	—	`ed.`	Proceedings of TLDI 2011: 2011 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Austin, TX, USA, January 25, 2011 TLDI Stephanie Weirich, Derek Dreyer
2011	A*	`conf`	Separation Logic in the Presence of Garbage Collection. LICS Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis
2010	A*	`conf`	A relational modal logic for higher-order stateful ADTs. POPL Derek Dreyer, Georg Neis, Andreas Rossberg, Lars Birkedal
2010	—	`conf`	F-ing modules. TLDI Andreas Rossberg, Claudio V. Russo, Derek Dreyer
2010	A	`conf`	The impact of higher-order state and control effects on local relational reasoning. ICFP Derek Dreyer, Georg Neis, Lars Birkedal
2009	A*	`conf`	Logical Step-Indexed Logical Relations. LICS Derek Dreyer, Amal Ahmed, Lars Birkedal
2009	A	`conf`	Non-parametric parametricity. ICFP Georg Neis, Derek Dreyer, Andreas Rossberg
2009	A*	`conf`	State-dependent representation independence. POPL Amal Ahmed, Derek Dreyer, Andreas Rossberg
2008	A	`conf`	Mixin' up the ML module system. ICFP Derek Dreyer, Andreas Rossberg
2007	A	`conf`	A type system for recursive modules. ICFP Derek Dreyer
2007	A*	`conf`	Modular type classes. POPL Derek Dreyer, Robert Harper, Manuel M. T. Chakravarty, Gabriele Keller
2007	A	`conf`	Principal Type Schemes for Modular Programs. ESOP Derek Dreyer, Matthias Blume
2007	—	`ed.`	Proceedings of the ACM Workshop on ML, 2007, Freiburg, Germany, October 5, 2007 ML Claudio V. Russo, Derek Dreyer
2007	J	`jnl`	Recursive type generativity. J. Funct. Program. Derek Dreyer
2005	A	`conf`	Recursive type generativity. ICFP Derek Dreyer
2004	A*	`conf`	A type system for well-founded recursion. POPL Derek Dreyer
2003	A*	`conf`	A type system for higher-order modules. POPL Derek Dreyer, Karl Crary, Robert Harper
2003	—	`conf`	Typed compilation of recursive datatypes. TLDI Joseph Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, Perry Cheng