Rasmus Ejlers Møgelberg

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)


Contact information

Address: Rasmus Ejlers Møgelberg
IT University of Copenhagen
Rued Langgaards Vej 7
2300 Copenhagen S
Denmark
Email: mogel[at]itu.dk

PhD Students

Christian Uldal Graulund (started 2016)

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

Postdocs

Bassel Mannaa (from Oct 2016)

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


Current projects

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).


Research

Papers

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).

Technical reports and unpublished papers

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

Dissertations

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

A poster

L. Birkedal, R.E. Møgelberg, R.L. Petersen: Parametricity Poster pdf