| RustBelt: Securing the foundations of the Rust programming language R Jung, JH Jourdan, R Krebbers, D Dreyer POPL, 2018 | 645 | 2018 |
| 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 JFP, 2018 | 644 | 2018 |
| Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning R Jung, D Swasey, F Sieczkowski, K Svendsen, A Turon, L Birkedal, ... POPL, 2015 | 507 | 2015 |
| Repairing sequential consistency in C/C++ 11 O Lahav, V Vafeiadis, J Kang, CK Hur, D Dreyer PLDI, 2017 | 290 | 2017 |
| A Promising Semantics for Relaxed-Memory Concurrency J Kang, CK Hur, O Lahav, V Vafeiadis, D Dreyer POPL, 2017 | 265 | 2017 |
| State-dependent representation independence A Ahmed, D Dreyer, A Rossberg POPL, 2009 | 243 | 2009 |
| The Essence of Higher-Order Concurrent Separation Logic R Krebbers, R Jung, A Bizjak, JH Jourdan, D Dreyer, L Birkedal ESOP, 2017 | 206 | 2017 |
| Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency A Turon, D Dreyer, L Birkedal ICFP, 2013 | 202 | 2013 |
| Logical step-indexed logical relations D Dreyer, A Ahmed, L Birkedal Logical Methods in Computer Science 7, 2011 | 202 | 2011 |
| The impact of higher-order state and control effects on local relational reasoning D Dreyer, G Neis, L Birkedal JFP / ICFP, 2012 | 197 | 2012 |
| Higher-order ghost state R Jung, R Krebbers, L Birkedal, D Dreyer ICFP, 2016 | 196 | 2016 |
| GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation A Turon, V Vafeiadis, D Dreyer OOPSLA, 2014 | 181 | 2014 |
| Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris JO Kaiser, HH Dang, D Dreyer, O Lahav, V Vafeiadis ECOOP, 2017 | 165 | 2017 |
| 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 | 157 | 2013 |
| RefinedC: automating the foundational verification of C code with refined ownership types M Sammler, R Lepigre, R Krebbers, K Memarian, D Dreyer, D Garg Proceedings of the 42nd ACM SIGPLAN International Conference on Programming …, 2021 | 146 | 2021 |
| 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 | 140 | 2018 |
| Stacked borrows: an aliasing model for Rust R Jung, HH Dang, J Kang, D Dreyer Proceedings of the ACM on Programming Languages 4 (POPL), 41, 2020 | 134 | 2020 |
| 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 | 127 | 2011 |
| F-ing modules A Rossberg, C Russo, D Dreyer Journal of Functional Programming 24 (5), 529-607, 2014 | 121* | 2014 |
| 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 | 121 | 2003 |
Lars BirkedalDept. of Computer Science, Aarhus UniversityVerified email at cs.au.dk
