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
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
2142015
State-dependent representation independence
A Ahmed, D Dreyer, A Rossberg
ACM SIGPLAN Notices 44 (1), 340-353, 2009
1902009
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
1452012
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
1432018
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
1282013
Logical step-indexed logical relations
D Dreyer, A Ahmed, L Birkedal
arXiv preprint arXiv:1103.0510, 2011
1232011
GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation
A Turon, V Vafeiadis, D Dreyer
1162014
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, 2018
1142018
Repairing sequential consistency in C/C++ 11
O Lahav, V Vafeiadis, J Kang, CK Hur, D Dreyer
PLDI 2017, 2017
1122017
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
1092003
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
1062017
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
922013
The Essence of Higher-Order Concurrent Separation Logic
R Krebbers, R Jung, A Bizjak, JH Jourdan, D Dreyer, L Birkedal
ESOP, 2017
912017
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
902011
How to make ad hoc proof automation less ad hoc
G Gonthier, B Ziliani, A Nanevski, D Dreyer
Journal of Functional Programming 23 (4), 357-401, 2013
822013
F-ing modules
A Rossberg, C Russo, D Dreyer
Journal of Functional Programming 24 (5), 529-607, 2014
80*2014
Higher-order ghost state
R Jung, R Krebbers, L Birkedal, D Dreyer
Proceedings of the 21st ACM SIGPLAN International Conference on Functional …, 2016
782016
Mtac: A monad for typed tactic programming in coq
B ZILIANI, D DREYER, NR KRISHNASWAMI, A NANEVSKI, V VAFEIADIS
Journal of Functional Programming 25, e12, 2015
742015
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
722013
The marriage of bisimulations and Kripke logical relations
CK Hur, D Dreyer, G Neis, V Vafeiadis
Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2012
702012
El sistema no puede realizar la operación en estos momentos. Inténtalo de nuevo más tarde.
Artículos 1–20