I am an associate professor at the IT University of Copenhagen in the Computer Science Department, and member of the (unofficial) Programming, Logic and Semantics research interest 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 |

Christian Uldal Graulund (started 2016)

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

Niccolò Veltri (from Sept 2017)

Bassel Mannaa (from Oct 2016)

Patrick Bahr (2015-2016). Now assistant professor at ITU

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

Guarded recursive types in the foundations of programming (2015-2018). Funded by The Danish Council for Independent Research (FNU).

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.* To appear
in Mathematical Structures in Computer Science. 2018. arXiv

R. Clouston, B. Mannaa and R.E. Møgelberg, A. M. Pitts, and
B. Spitters: *Modal Dependent Type Theory and Dependent Right
Adjoints.* Submitted 2018. 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.* Manuscript 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