Follow
Lars Birkedal
Lars Birkedal
Dept. of Computer Science, Aarhus University
Verified email at cs.au.dk - Homepage
Title
Cited by
Cited by
Year
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
3432018
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
3412015
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
2192013
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
1992008
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
1981996
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
1962011
Polymorphism and separation in hoare type theory
A Nanevski, G Morrisett, L Birkedal
Proceedings of the eleventh ACM SIGPLAN international conference on†…, 2006
1782006
Hoare type theory, polymorphism and separation1
A Nanevski, G Morrisett, L Birkedal
Journal of Functional Programming 18 (5-6), 865-911, 2008
1752008
A region inference algorithm
M Tofte, L Birkedal
ACM Transactions on Programming Languages and Systems (TOPLAS) 20 (4), 724-767, 1998
1741998
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
1712013
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
1562017
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
1362017
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
1342006
Higher-order ghost state
R Jung, R Krebbers, L Birkedal, D Dreyer
Proceedings of the 21st ACM SIGPLAN International Conference on Functional†…, 2016
1232016
Equilogical spaces
A Bauer, L Birkedal, DS Scott
Theoretical Computer Science 315 (1), 35-59, 2004
1222004
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
1092011
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
1092007
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
1092004
A retrospective on region-based memory management
M Tofte, L Birkedal, M Elsman, N Hallenberg
Higher-Order and Symbolic Computation 17, 245-265, 2004
1062004
The system can't perform the operation now. Try again later.
Articles 1–20