Follow
Derek Dreyer
Derek Dreyer
Max Planck Institute for Software Systems (MPI-SWS), Saarland Informatics Campus
Verified email at mpi-sws.org - Homepage
Title
Cited by
Cited by
Year
Iris from the ground up: A modular foundation for higher-order concurrent separation logic
R Jung, R Krebbers, JH Jourdan, A Bizjak, L Birkedal, D Dreyer
Journal of Functional Programming 28, e20, 2018
4782018
RustBelt: Securing the foundations of the Rust programming language
R Jung, JH Jourdan, R Krebbers, D Dreyer
Proc. ACM Program. Lang. 2, POPL, Article, 2018
4762018
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
R Jung, D Swasey, F Sieczkowski, K Svendsen, A Turon, L Birkedal, ...
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of …, 2015
4122015
Repairing sequential consistency in C/C++ 11
O Lahav, V Vafeiadis, J Kang, CK Hur, D Dreyer
PLDI 2017, 2017
2402017
State-dependent representation independence
A Ahmed, D Dreyer, A Rossberg
ACM SIGPLAN Notices 44 (1), 340-353, 2009
2352009
A Promising Semantics for Relaxed-Memory Concurrency
J Kang, CK Hur, O Lahav, V Vafeiadis, D Dreyer
ACM Symp. on Principles of Programming Languages (POPL) 2017, 2017
2312017
The impact of higher-order state and control effects on local relational reasoning
D Dreyer, G Neis, L Birkedal
Journal of Functional Programming 22 (4-5), 477-528, 2012
1862012
Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
A Turon, D Dreyer, L Birkedal
Proceedings of the 18th ACM SIGPLAN international conference on Functional …, 2013
1832013
Logical step-indexed logical relations
D Dreyer, A Ahmed, L Birkedal
Logical Methods in Computer Science 7, 2011
1762011
The Essence of Higher-Order Concurrent Separation Logic
R Krebbers, R Jung, A Bizjak, JH Jourdan, D Dreyer, L Birkedal
ESOP, 2017
1692017
GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation
A Turon, V Vafeiadis, D Dreyer
1642014
Higher-order ghost state
R Jung, R Krebbers, L Birkedal, D Dreyer
Proceedings of the 21st ACM SIGPLAN International Conference on Functional …, 2016
1562016
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris
JO Kaiser, HH Dang, D Dreyer, O Lahav, V Vafeiadis
1422017
The power of parameterization in coinductive proof
CK Hur, G Neis, D Dreyer, V Vafeiadis
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2013
1342013
A type system for higher-order modules
D Dreyer, K Crary, R Harper
Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of …, 2003
1202003
A Kripke logical relation between ML and assembly
CK Hur, D Dreyer
Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2011
1152011
F-ing modules
A Rossberg, C Russo, D Dreyer
Journal of Functional Programming 24 (5), 529-607, 2014
114*2014
Logical relations for fine-grained concurrency
AJ Turon, J Thamsborg, A Ahmed, L Birkedal, D Dreyer
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2013
1112013
MoSeL: A general, extensible modal framework for interactive proofs in separation logic
R Krebbers, JH Jourdan, R Jung, J Tassarotti, JO Kaiser, A Timany, ...
Proceedings of the ACM on Programming Languages 2 (ICFP), 77, 2018
1042018
Pilsner: A compositionally verified compiler for a higherorder imperative language
G Neis, CK Hur, JO Kaiser, C McLaughlin, D Dreyer, V Vafeiadis
Proceedings of the 20th ACM SIGPLAN International Conference on Functional …, 2015
1022015
The system can't perform the operation now. Try again later.
Articles 1–20