First steps in synthetic guarded domain theory: step-indexing in the topos of trees L Birkedal, RE Møgelberg, J Schwinghammer, K Støvring Logical Methods in Computer Science 8, 2012 | 212 | 2012 |
Guarded dependent type theory with coinductive types A Bizjak, HB Grathwohl, R Clouston, RE Møgelberg, L Birkedal International Conference on Foundations of Software Science and Computation …, 2016 | 85 | 2016 |
Modal dependent type theory and dependent right adjoints L Birkedal, R Clouston, B Mannaa, RE Møgelberg, AM Pitts, B Spitters Mathematical Structures in Computer Science 30 (2), 118-138, 2020 | 59 | 2020 |
Intensional type theory with guarded recursive types qua fixed points on universes L Birkedal, RE Møgelberg 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 213-222, 2013 | 56 | 2013 |
The clocks are ticking: No more delays! P Bahr, HB Grathwohl, RE Møgelberg 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-12, 2017 | 53 | 2017 |
A type theory for productive coprogramming via guarded recursion RE Møgelberg Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference …, 2014 | 53 | 2014 |
The enriched effect calculus: syntax and semantics J Egger, R Ejlers, A Simpson Journal of Logic and Computation 24 (3), 615-654, 2014 | 49 | 2014 |
Categorical models for Abadi and Plotkin's logic for parametricity L Birkedal, RE Møgelberg Mathematical Structures in Computer Science 15 (4), 709-772, 2005 | 45 | 2005 |
Enriching an effect calculus with linear types J Egger, RE Møgelberg, A Simpson Computer Science Logic: 23rd international Workshop, CSL 2009, 18th Annual …, 2009 | 41 | 2009 |
Linear usage of state RE Møgelberg, S Staton Logical Methods in Computer Science 10, 2014 | 35 | 2014 |
Relational parametricity for computational effects RE Møgelberg, A Simpson Logical Methods in Computer Science 5, 2009 | 35* | 2009 |
Simply RaTT: a fitch-style modal calculus for reactive programming without space leaks P Bahr, CU Graulund, RE Møgelberg Proceedings of the ACM on Programming Languages 3 (ICFP), 1-27, 2019 | 34 | 2019 |
Denotational semantics of recursive types in synthetic guarded domain theory RE Møgelberg, M Paviotti Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer …, 2016 | 32 | 2016 |
A model of PCF in guarded type theory M Paviotti, RE Møgelberg, L Birkedal Electronic Notes in Theoretical Computer Science 319, 333-349, 2015 | 32 | 2015 |
Linear abadi and plotkin logic L Birkedal, RE Møgelberg, RL Petersen Logical Methods in Computer Science 2, 2006 | 27 | 2006 |
A model of guarded recursion with clock synchronisation A Bizjak, RE Møgelberg Electronic Notes in Theoretical Computer Science 319, 83-101, 2015 | 25 | 2015 |
Bisimulation as path type for guarded recursive types RE Møgelberg, N Veltri Proceedings of the ACM on Programming Languages 3 (POPL), 1-29, 2019 | 24 | 2019 |
Denotational semantics for guarded dependent type theory A Bizjak, RE Møgelberg Mathematical Structures in Computer Science 30 (4), 342-378, 2020 | 23 | 2020 |
Diamonds are not forever: liveness in reactive programming with guarded recursion P Bahr, CU Graulund, RE Møgelberg Proceedings of the ACM on Programming Languages 5 (POPL), 1-28, 2021 | 20 | 2021 |
The clocks they are adjunctions: Denotational semantics for clocked type theory B Mannaa, RE Møgelberg arXiv preprint arXiv:1804.06687, 2018 | 16 | 2018 |