Seguir
Derek Dreyer
Derek Dreyer
Max Planck Institute for Software Systems (MPI-SWS), Saarland Informatics Campus
Dirección de correo verificada de mpi-sws.org - Página principal
Título
Citado por
Citado por
Año
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
5022018
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
5002018
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
4242015
Repairing sequential consistency in C/C++ 11
O Lahav, V Vafeiadis, J Kang, CK Hur, D Dreyer
PLDI 2017, 2017
2492017
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
2372017
State-dependent representation independence
A Ahmed, D Dreyer, A Rossberg
ACM SIGPLAN Notices 44 (1), 340-353, 2009
2352009
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
1872012
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
1852013
Logical step-indexed logical relations
D Dreyer, A Ahmed, L Birkedal
Logical Methods in Computer Science 7, 2011
1772011
The Essence of Higher-Order Concurrent Separation Logic
R Krebbers, R Jung, A Bizjak, JH Jourdan, D Dreyer, L Birkedal
ESOP, 2017
1752017
GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation
A Turon, V Vafeiadis, D Dreyer
1662014
Higher-order ghost state
R Jung, R Krebbers, L Birkedal, D Dreyer
Proceedings of the 21st ACM SIGPLAN International Conference on Functional …, 2016
1612016
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris
JO Kaiser, HH Dang, D Dreyer, O Lahav, V Vafeiadis
1482017
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
1372013
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
F-ing modules
A Rossberg, C Russo, D Dreyer
Journal of Functional Programming 24 (5), 529-607, 2014
117*2014
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
1162011
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
1122013
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
1082018
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
1032015
El sistema no puede realizar la operación en estos momentos. Inténtalo de nuevo más tarde.
Artículos 1–20