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 (started 2019)

Christian Uldal Graulund (2016-2021). Thesis: Type Theories for Reactive Programming

Marco Paviotti (graduated 2016). Thesis: Denotational Semantics in Guarded Type Theory

Andrea Vezzosi (Feb 2019 - 2021)

Niccolò 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

Type theories for reactive programming (2016-2021). Funded by Villum Fonden.

R.E. Møgelberg and A. Vezzosi: *Two Guarded Recursive Powerdomains for Applicative Simulation.*
MFPS, 2021. Available here

M.B. Kristensen, R.E. Møgelberg and A. Vezzosi: *Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks.*
Manuscript, 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

P. Bahr, C. Graulund and R.E. Møgelberg: *Diamonds are
not forever: Liveness in reactive programming with guarded
recursion.* POPL 2021. arXiv

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

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

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

B. Mannaa and R.E. Møgelberg: *The clocks they are
adjunctions: Denotational semantics for Clocked Type Theory.* FSCD 2018. 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, 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