I am an associate professor at the IT University of Copenhagen in the Computer Science Department, and coordinator of the Programming, Logic and Semantics research group.
Research area: Denotational semantics of programming languages, type theory, category theory, guarded recursion, domain theory, logic, parametric polymorphism, computational effects
Former affiliations: PhD student and later postdoc at IT University of Copenhagen (2002 - 2005), postdoc at DISI, Universita di Genova (2005 - 2006), post doc. at LFCS, University of Edinburgh (2006 - 2007)
| Address: | Rasmus Ejlers Møgelberg |
| IT University of Copenhagen | |
| Rued Langgaards Vej 7 | |
| 2300 Copenhagen S | |
| Denmark | |
| Email: | mogel[at]itu.dk |
Magnus Baunsgaard Kristensen (2019 - 2022). Thesis: Cubical Modal Type Theories
Christian Uldal Graulund (2016-2021). Thesis: Type Theories for Reactive Programming
Marco Paviotti (graduated 2016). Thesis: Denotational Semantics in Guarded Type Theory
Maaike Zwart (Sept 2021 - now)
Andrea Vezzosi (Feb 2019 - 2021). Now at MLabs Consultancy
Niccolo Veltri (2017-2019). Now at Tallinn University of Technology
Bassel Mannaa (Oct 2016 - 2018). Now at eToroX Labs
Patrick Bahr (2015-2016). Now associate professor at ITU
Algebraic Effects and Guarded Recursion (2022-2025). Funded by Independent Research Fund Denmark.
P.J.A. Stassen, R.E. Møgelberg, M. Zwart, A. Aguirre, L. Birkedal: Modelling Recursion and Probabilistic Choice in Guarded Type Theory. POPL 2025. arXiv
R.E. Møgelberg and M. Zwart: What monads can and cannot do with a bit of extra time. CSL 2024. arXiv
P. Bahr and R.E. Møgelberg: Asynchronous Modal FRP. ICFP 2023. arXiv
M.B. Kristensen, R.E. Møgelberg and A. Vezzosi: Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks. LICS 2022. arXiv
R.E. Møgelberg and A. Vezzosi: Two Guarded Recursive Powerdomains for Applicative Simulation. MFPS, 2021. Available here
P. Bahr, C. Graulund and R.E. Møgelberg: Diamonds are not forever: Liveness in reactive programming with guarded recursion. POPL 2021. arXiv
B. Mannaa, R.E. Møgelberg and N. Veltri: Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory. Logical Methods in Computer Science, Volume 16, issue 4, 2020. Open access here
A.S. Al-Sibahi, T. Jensen, R.E. Møgelberg and A. Wasowski: Galois Connections for Recursive Types. From Lambda Calculus to Cybersecurity Through Program Analysis, pp 105-131, 2020. paper
R. Clouston, B. Mannaa and R.E. Møgelberg, A. M. Pitts, and B. Spitters: Modal Dependent Type Theory and Dependent Right Adjoints. Mathematical Structures in Computer Science, vol 30, issue 2, pp 118-138, 2020. arXiv
A. Bizjak and R.E. Møgelberg: Denotational semantics for guarded dependent type theory. Mathematical Structures in Computer Science, vol 30, issue 4, pp 342-378, 2020. arXiv
P. Bahr, C. Graulund and R.E. Møgelberg: Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming. ICFP 2019. paper , arXiv
R.E. Møgelberg and N. Veltri: Bisimulation as path type for guarded recursive types. POPL 2019. arXiv
M. Paviotti and R.E. Møgelberg: Denotational semantics of recursive types in synthetic guarded domain theory. Mathematical Structures in Computer Science, vol 29, issue 3, pp 465-510, 2019. arXiv
B. Mannaa and R.E. Møgelberg: The clocks they are adjunctions: Denotational semantics for Clocked Type Theory. FSCD 2018. arXiv
P. Bahr, H.B. Grathwohl and R.E. Møgelberg: The Clocks Are Ticking: No More Delays! Reduction Semantics for Type Theory with Guarded Recursion. LICS 2017. pdf
R.E. Møgelberg and M. Paviotti: Denotational semantics of recursive types in synthetic guarded domain theory. LICS 2016. pdf
A. Bizjak, H.B. Grathwohl, R.Clouston, R.E. Møgelberg and L. Birkedal: Guarded Dependent Type Theory with Coinductive Types. FoSSaCS 2016. pdf
A. Bizjak and R.E. Møgelberg: A model of guarded recursion with clock synchronisation. MFPS 2015. pdf
M. Paviotti, R.E. Møgelberg and L. Birkedal: A Model of PCF in Guarded Type Theory. MFPS 2015. pdf
R.E. Møgelberg: A type theory for productive coprogramming via guarded recursion. LICS-CSL 2014. pdf
R.E. Møgelberg and S. Staton: Linear usage of state. Journal version of CALCO 2011 paper. Logical Methods in Computer Science, Volume 10, issue 1. March 2014. Available for free download at the LMCS homepage
L. Birkedal and R.E. Møgelberg: Intensional type theory with guarded recursive types qua fixed points on universes. LICS 2013. pdf
L. Birkedal, R.E. Møgelberg, J. Schwinghammer, K. Støvring: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Journal version on LICS 2011 paper. Logical Methods in Computer Science, Volume 8, issue 4. October 2012. Available for free download at the LMCS homepage,
J. Egger, R.E. Møgelberg and A. Simpson: The Enriched Effect Calculus: Syntax and Semantics. Journal of Logic and Computation. Journal version of CSL 2009 paper. Published online June 2012. pdf
J. Egger, R.E. Møgelberg and A. Simpson: Linear-use CPS translations in the enriched effect calculus. Journal version of FoSSaCS 2010 paper. Logical Methods in Computer Science, Volume 8, issue 4. October 2012. Available for free download at the LMCS homepage
R.E. Møgelberg, S. Staton: Linearly-used state in models of call-by-value. CALCO 2011. pdf
L. Birkedal, R.E. Møgelberg, J. Schwinghammer, K. Støvring: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. LICS 2011. pdf
R.E. Møgelberg: A nominal relational model for local store. MFPS 2010.pdf
J. Egger, R.E. Møgelberg and A. Simpson: Linearly-used Continuations in the Enriched Effect Calculus. FoSSaCS 2010. pdf
J. Egger, R.E. Møgelberg and A. Simpson: Enriching an Effect Calculus with Linear Types. CSL 2009. pdf
R.E. Møgelberg and A.Simpson: Relational Parametricity for Computational Effects. Logical Methods in Computer Science, Volume 5, issue 3. August 2009. Available for free download at the LMCS homepage,
R.E. Møgelberg and A. Simpson: A logic for parametric polymorphism with effects. Types 2007. pdf
R.E. Møgelberg and A. Simpson: Relational Parametricity for Computational Effects. LICS 2007. ps, pdf
R.E. Møgelberg and A. Simpson: Relational Parametricity for Control Considered as a Computational Effect. December 2006. MFPS 2007.ps, pdf
R.E. Møgelberg: From parametric polymorphism to models of polymorphic FPC. Mathematical Structures in Computer Science, 19(4): 639-686, 2009pdf
R.E. Møgelberg, L. Birkedal and G. Rosolini: Synthetic domain theory and models of linear Abadi & Plotkin logic. Annals of Pure and Applied Logic, 155(2):115-133, 2008 ps, pdf
L. Birkedal, R.E. Møgelberg and R.L. Petersen: Domain theoretic models of parametric polymorphism. Theoretical Computer Science, 388, 2007. ps, pdf
L. Birkedal, R.E. Møgelberg and R.L. Petersen: Category theoretic models of Linear Abadi & Plotkin Logic. Theory and Applications of Categories, 20, 2008.
L. Birkedal, R.E. Møgelberg and R.L. Petersen: Linear Abadi & Plotkin Logic. Logical Methods in Computer Science, Volume 2, issue 5. November 2006. Available for free download at the LMCS homepage,
R.E. Møgelberg: Interpreting polymorphic FPC into domain theoretic models of parametric polymorphism. ICALP 2006 ps, pdf
R.E. Møgelberg, L. Birkedal and G. Rosolini: Synthetic domain theory and models of linear Abadi & Plotkin logic. Mathematical Foundations of Programming Semantics XXI, 25 pages. Feb 2005 ps, pdf
L. Birkedal, R.E. Møgelberg and R.L. Petersen: Parametric Domain-theoretic models of polymorphic intuitionistic / linear lambda calculus. Mathematical Foundations of Programming Semantics XXI, 25 pages. Feb 2005 ps, pdf
L. Birkedal and R.E. Møgelberg: Categorical Models of Abadi-Plotkin's logic for parametricity. Mathematical Structures in Computer Science, 15(4):709-772, 2005. ps, pdf
R.E. Møgelberg: A natural classifying space for cohomology with coefficients in a finite chain complex, Topology Proceedings Volume 28 Number 1 (2004).
R.E. Møgelberg: Parametric completion for models of polymorphic linear / intuitionistic lambda calculus. Technical Report, 27 pages. Feb 2005 ps, pdf
R.E. Møgelberg, L. Birkedal and G. Rosolini: Synthetic domain theory and models of linear Abadi & Plotkin logic. Technical Report, 50 pages. Feb 2005 ps, pdf
L. Birkedal, R.E. Møgelberg and R.L. Petersen: Parametric Domain-theoretic models of Linear Abadi & Plotkin Logic. Technical Report, 76 pages. Feb 2005 ps, pdf
R.E. Møgelberg, L. Birkedal and R.L. Petersen: Categorical models of PILL. Technical Report, 15 pages. Feb 2005 ps, pdf
L. Birkedal and R.E. Møgelberg: Categorical models of parametric polymorphism. Manuscript, 11 pages. Feb 2004. ps
R.E. Møgelberg: Categorical and domain theoretic models of parametric polymorphism. PhD dissertation, IT University of Copenhagen, 271 pages. Revised August 2005 pdf
R.E. Møgelberg: A natural classifying space for cohomology with coefficients in a finite chain complex, Master thesis, University of Copenhagen, Feb 2002. ps, pdf
L. Birkedal, R.E. Møgelberg, R.L. Petersen: Parametricity Poster pdf