| 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 | 343 | 2018 |
| Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning R Jung, D Swasey, F Sieczkowski, K Svendsen, A Turon, L Birkedal, ... ACM SIGPLAN Notices 50 (1), 637-650, 2015 | 341 | 2015 |
| Views: compositional reasoning for concurrent programs T Dinsdale-Young, L Birkedal, P Gardner, M Parkinson, H Yang Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on principles of …, 2013 | 219 | 2013 |
| Impredicative concurrent abstract predicates K Svendsen, L Birkedal Programming Languages and Systems: 23rd European Symposium on Programming …, 2014 | 205* | 2014 |
| Ynot: dependent types for imperative programs A Nanevski, G Morrisett, A Shinnar, P Govereau, L Birkedal Proceedings of the 13th ACM SIGPLAN international conference on Functional …, 2008 | 199 | 2008 |
| From region inference to von Neumann machines via region representation inference L Birkedal, M Tofte, M Vejlstrup Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of …, 1996 | 198 | 1996 |
| First steps in synthetic guarded domain theory: step-indexing in the topos of trees L Birkedal, RE Mogelberg, J Schwinghammer, K Stovring 2011 IEEE 26th Annual Symposium on Logic in Computer Science, 55-64, 2011 | 196 | 2011 |
| Polymorphism and separation in hoare type theory A Nanevski, G Morrisett, L Birkedal Proceedings of the eleventh ACM SIGPLAN international conference on …, 2006 | 178 | 2006 |
| Hoare type theory, polymorphism and separation1 A Nanevski, G Morrisett, L Birkedal Journal of Functional Programming 18 (5-6), 865-911, 2008 | 175 | 2008 |
| A region inference algorithm M Tofte, L Birkedal ACM Transactions on Programming Languages and Systems (TOPLAS) 20 (4), 724-767, 1998 | 174 | 1998 |
| 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 | 171 | 2013 |
| Interactive proofs in higher-order concurrent separation logic R Krebbers, A Timany, L Birkedal Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming …, 2017 | 156 | 2017 |
| The essence of higher-order concurrent separation logic R Krebbers, R Jung, A Bizjak, JH Jourdan, D Dreyer, L Birkedal Programming Languages and Systems: 26th European Symposium on Programming …, 2017 | 136 | 2017 |
| Bigraphical models of context-aware systems L Birkedal, S Debois, E Elsborg, T Hildebrandt, H Niss Foundations of Software Science and Computation Structures: 9th …, 2006 | 134 | 2006 |
| Higher-order ghost state R Jung, R Krebbers, L Birkedal, D Dreyer Proceedings of the 21st ACM SIGPLAN International Conference on Functional …, 2016 | 123 | 2016 |
| Equilogical spaces A Bauer, L Birkedal, DS Scott Theoretical Computer Science 315 (1), 35-59, 2004 | 122 | 2004 |
| Step-indexed Kripke models over recursive worlds L Birkedal, B Reus, J Schwinghammer, K Støvring, J Thamsborg, H Yang ACM SIGPLAN Notices 46 (1), 119-132, 2011 | 109 | 2011 |
| BI-hyperdoctrines, higher-order separation logic, and abstraction B Biering, L Birkedal, N Torp-Smith ACM Transactions on Programming Languages and Systems (TOPLAS) 29 (5), 24-es, 2007 | 109 | 2007 |
| Local reasoning about a copying garbage collector L Birkedal, N Torp-Smith, JC Reynolds Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of …, 2004 | 109 | 2004 |
| A retrospective on region-based memory management M Tofte, L Birkedal, M Elsman, N Hallenberg Higher-Order and Symbolic Computation 17, 245-265, 2004 | 106 | 2004 |
