Folgen
Derek Dreyer
Derek Dreyer
Max Planck Institute for Software Systems (MPI-SWS), Saarland Informatics Campus
Bestätigte E-Mail-Adresse bei mpi-sws.org - Startseite
Titel
Zitiert von
Zitiert von
Jahr
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
3992018
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
3842018
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
3722015
State-dependent representation independence
A Ahmed, D Dreyer, A Rossberg
ACM SIGPLAN Notices 44 (1), 340-353, 2009
2242009
Repairing sequential consistency in C/C++ 11
O Lahav, V Vafeiadis, J Kang, CK Hur, D Dreyer
PLDI 2017, 2017
2112017
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
2002017
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
1802012
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
1792013
Logical step-indexed logical relations
D Dreyer, A Ahmed, L Birkedal
Logical Methods in Computer Science 7, 2011
1632011
GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation
A Turon, V Vafeiadis, D Dreyer
1602014
The Essence of Higher-Order Concurrent Separation Logic
R Krebbers, R Jung, A Bizjak, JH Jourdan, D Dreyer, L Birkedal
ESOP, 2017
1512017
Higher-order ghost state
R Jung, R Krebbers, L Birkedal, D Dreyer
Proceedings of the 21st ACM SIGPLAN International Conference on Functional …, 2016
1402016
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris
JO Kaiser, HH Dang, D Dreyer, O Lahav, V Vafeiadis
1282017
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
1242013
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
1162003
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
1082011
F-ing modules
A Rossberg, C Russo, D Dreyer
Journal of Functional Programming 24 (5), 529-607, 2014
105*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
1032013
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
962015
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
962013
Das System kann den Vorgang jetzt nicht ausführen. Versuchen Sie es später erneut.
Artikel 1–20