| 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 1, 2018 | 502 | 2018 |
| 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 | 175 | 2017 |
| Guarded Dependent Type Theory with Coinductive Types A Bizjak, R Clouston, HB Grathwohl, L Birkedal | 86* | |
| Guarded cubical type theory: Path equality for guarded recursion L Birkedal, A Bizjak, R Clouston, HB Grathwohl, B Spitters, A Vezzosi arXiv preprint arXiv:1606.05223, 2016 | 73* | 2016 |
| Step-Indexed Logical Relations for Probability A Bizjak, L Birkedal Foundations of Software Science and Computation Structures 9034, 279-294, 2015 | 63 | 2015 |
| Programming and reasoning with guarded recursion for coinductive types R Clouston, A Bizjak, HB Grathwohl, L Birkedal Foundations of Software Science and Computation Structures 9034, 407-421, 2015 | 44 | 2015 |
| The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types R Clouston, A Bizjak, HB Grathwohl, L Birkedal Logical Methods in Computer Science, 2016 | 36 | 2016 |
| Iron: Managing obligations in higher-order concurrent separation logic A Bizjak, D Gratzer, R Krebbers, L Birkedal https://iris-project.org/pdfs/2019-popl-iron-final.pdf, 2018 | 35 | 2018 |
| A model of countable nondeterminism in guarded type theory A Bizjak, L Birkedal, M Miculan Rewriting and Typed Lambda Calculi 8560, 108-123, 2014 | 31 | 2014 |
| On models of higher-order separation logic A Bizjak, L Birkedal Electronic Notes in Theoretical Computer Science 336, 57-78, 2018 | 25 | 2018 |
| A model of guarded recursion with clock synchronisation A Bizjak, RE Møgelberg Mathematical Foundations of Programming Semantics, 2015 | 25 | 2015 |
| Denotational semantics for guarded dependent type theory A Bizjak, RE Møgelberg Mathematical Structures in Computer Science 30 (4), 342-378, 2020 | 24 | 2020 |
| Step-indexed relational reasoning for countable nondeterminism L Birkedal, A Bizjak, J Schwinghammer Logical Methods in Computer Science 9 (4), 2013 | 21* | 2013 |
| Relational reasoning for markov chains in a probabilistic guarded lambda calculus A Aguirre, G Barthe, L Birkedal, A Bizjak, M Gaboardi, D Garg Programming Languages and Systems: 27th European Symposium on Programming …, 2018 | 20 | 2018 |
| ModuRes: a Coq Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming Languages F Sieczkowski, A Bizjak, L Birkedal Interactive Theorem Proving, 2015 | 17 | 2015 |
| Lecture notes on iris: Higher-order concurrent separation logic L Birkedal, A Bizjak Lectures notes, September, 2020 | 16 | 2020 |
| A Taste of Categorical Logic—tutorial notes L Birkedal, A Bizjak | 10 | 2014 |
| On semantics and applications of guarded recursion A Bizjak Department of Computer Science, Aarhus University, 2016 | 8 | 2016 |
| Alg user manual A Bizjak, A Bauer Faculty of Mathematics and Physics, University of Ljubljana, 2011 | 5 | 2011 |
| Some theorems about mutually recursive domain equations in the category of preordered COFEs A Bizjak Unpublished note. Available at http://cs. au. dk/~ abizjak/documents/notes …, 2017 | 4 | 2017 |
Lars BirkedalDept. of Computer Science, Aarhus UniversityE-mail confirmado em cs.au.dk
