Parametric Domain-theoretic Models of Polymorphic Intuitionistic / Linear Lambda Calculus. - Lars Birkedal; Rasmus Ejlers Møgelberg; Rasmus Lerchedahl Petersen (MFPS, 2005)

Synthetic Domain Theory and Models of Linear Abadi & Plotkin Logic. - Rasmus Ejlers Møgelberg; Lars Birkedal; Giuseppe Rosolini (MFPS, 2005)

Categorical models for Abadi and Plotkin's logic for parametricity. - Lars Birkedal; Rasmus Ejlers Møgelberg (Math. Struct. Comput. Sci., 2005)

Interpreting Polymorphic FPC into Domain Theoretic Models of Parametric Polymorphism. - Rasmus Ejlers Møgelberg (ICALP (2), 2006)

Linear Abadi and Plotkin Logic. - Lars Birkedal; Rasmus Ejlers Møgelberg; Rasmus Lerchedahl Petersen (Log. Methods Comput. Sci., 2006)

A Logic for Parametric Polymorphism with Effects. - Rasmus Ejlers Møgelberg; Alex Simpson (TYPES, 2007)

Relational Parametricity for Control Considered as a Computational Effect. - Rasmus Ejlers Møgelberg; Alex Simpson (MFPS, 2007)

Domain-theoretical models of parametric polymorphism. - Lars Birkedal; Rasmus Ejlers Møgelberg; Rasmus Lerchedahl Petersen (Theor. Comput. Sci., 2007)

Enriching an Effect Calculus with Linear Types. - Jeff Egger; Rasmus Ejlers Møgelberg; Alex Simpson (CSL, 2009)

Relational Parametricity for Computational Effects - Rasmus Ejlers Møgelberg; Alex Simpson (Log. Methods Comput. Sci., 2009)

From parametric polymorphism to models of polymorphic FPC. - Rasmus Ejlers Møgelberg (Math. Struct. Comput. Sci., 2009)

Linearly-Used Continuations in the Enriched Effect Calculus. - Jeff Egger; Rasmus Ejlers Møgelberg; Alex Simpson (FoSSaCS, 2010)

A Nominal Relational Model for Local Store. - Rasmus Ejlers Møgelberg (MFPS, 2010)

Linearly-Used State in Models of Call-by-Value. - Rasmus Ejlers Møgelberg; Sam Staton (CALCO, 2011)

First steps in synthetic guarded domain theory: step-indexing in the topos of trees - Lars Birkedal; Rasmus Ejlers Møgelberg; Jan Schwinghammer; Kristian Støvring (Log. Methods Comput. Sci., 2012)

Linear-use CPS translations in the Enriched Effect Calculus - Jeff Egger; Rasmus Ejlers Møgelberg; Alex Simpson (Log. Methods Comput. Sci., 2012)

Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes. - Lars Birkedal; Rasmus Ejlers Møgelberg (LICS, 2013)

A type theory for productive coprogramming via guarded recursion. - Rasmus Ejlers Møgelberg (CSL-LICS, 2014)

Linear usage of state. - Rasmus Ejlers Møgelberg; Sam Staton (Log. Methods Comput. Sci., 2014)

The enriched effect calculus: syntax and semantics. - Jeff Egger; Rasmus Ejlers Møgelberg; Alex Simpson (J. Log. Comput., 2014)

A Model of Guarded Recursion With Clock Synchronisation. - Ales Bizjak; Rasmus Ejlers Møgelberg (MFPS, 2015)

A Model of PCF in Guarded Type Theory. - Marco Paviotti; Rasmus Ejlers Møgelberg; Lars Birkedal (MFPS, 2015)

Guarded Dependent Type Theory with Coinductive Types. - Ales Bizjak; Hans Bugge Grathwohl; Ranald Clouston; Rasmus Ejlers Møgelberg; Lars Birkedal (FoSSaCS, 2016)

The clocks are ticking: No more delays! - Patrick Bahr; Hans Bugge Grathwohl; Rasmus Ejlers Møgelberg (LICS, 2017)

The Clocks They Are Adjunctions Denotational Semantics for Clocked Type Theory. - Bassel Mannaa; Rasmus Ejlers Møgelberg (FSCD, 2018)

Modal Dependent Type Theory and Dependent Right Adjoints. - Ranald Clouston; Bassel Mannaa; Rasmus Ejlers Møgelberg; Andrew M. Pitts; Bas Spitters (CoRR, 2018)

Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming. - Patrick Bahr; Christian Graulund; Rasmus Ejlers Møgelberg (CoRR, 2019)

Denotational semantics of recursive types in synthetic guarded domain theory. - Rasmus Ejlers Møgelberg; Marco Paviotti (Math. Struct. Comput. Sci., 2019)

Simply RaTT: a fitch-style modal calculus for reactive programming without space leaks. - Patrick Bahr; Christian Graulund; Rasmus Ejlers Møgelberg (Proc. ACM Program. Lang., 2019)

Bisimulation as path type for guarded recursive types. - Rasmus Ejlers Møgelberg; Niccolò Veltri (Proc. ACM Program. Lang., 2019)

Galois Connections for Recursive Types. - Ahmad Salim Al-Sibahi; Thomas P. Jensen; Rasmus Ejlers Møgelberg; Andrzej Wasowski (From Lambda Calculus to Cybersecurity Through Program Analysis, 2020)

Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory. - Bassel Mannaa; Rasmus Ejlers Møgelberg; Niccolò Veltri (Log. Methods Comput. Sci., 2020)

Modal dependent type theory and dependent right adjoints. - Lars Birkedal; Ranald Clouston; Bassel Mannaa; Rasmus Ejlers Møgelberg; Andrew M. Pitts; Bas Spitters (Math. Struct. Comput. Sci., 2020)

Denotational semantics for guarded dependent type theory. - Ales Bizjak; Rasmus Ejlers Møgelberg (Math. Struct. Comput. Sci., 2020)

A model of Clocked Cubical Type Theory. - Magnus Baunsgaard Kristensen; Rasmus Ejlers Møgelberg; Andrea Vezzosi (CoRR, 2021)

Two Guarded Recursive Powerdomains for Applicative Simulation. - Rasmus Ejlers Møgelberg; Andrea Vezzosi (MFPS, 2021)

Diamonds are not forever: liveness in reactive programming with guarded recursion. - Patrick Bahr; Christian Uldal Graulund; Rasmus Ejlers Møgelberg (Proc. ACM Program. Lang., 2021)

Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks. - Magnus Baunsgaard Kristensen; Rasmus Ejlers Møgelberg; Andrea Vezzosi (LICS, 2022)

Asynchronous Modal FRP. - Patrick Bahr; Rasmus Ejlers Møgelberg (Proc. ACM Program. Lang., 2023)

What Monads Can and Cannot Do with a Bit of Extra Time. - Rasmus Ejlers Møgelberg; Maaike Zwart (CSL, 2024)

Modelling Probabilistic FPC in Guarded Type Theory. - Philipp Stassen; Rasmus Ejlers Møgelberg; Maaike Zwart; Alejandro Aguirre 001; Lars Birkedal (CoRR, 2024)

Modelling Recursion and Probabilistic Choice in Guarded Type Theory. - Philipp Stassen; Rasmus Ejlers Møgelberg; Maaike Zwart; Alejandro Aguirre 001; Lars Birkedal (Proc. ACM Program. Lang., 2025)

Induction and Recursion Principles in a Higher-Order Quantitative Logic. - Giorgio Bacci; Rasmus Ejlers Møgelberg (CoRR, 2025)