Search Results

Documents authored by Møgelberg, Rasmus Ejlers

Document
Complete Volume
DOI: 10.4230/LIPIcs.TYPES.2024
LIPIcs, Volume 336, TYPES 2024, Complete Volume

Authors: Rasmus Ejlers Møgelberg and Benno van den Berg

Published in: LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024)

Abstract
LIPIcs, Volume 336, TYPES 2024, Complete Volume
Cite as

30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 1-190, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Proceedings{mogelberg_et_al:LIPIcs.TYPES.2024,
  title =	{{LIPIcs, Volume 336, TYPES 2024, Complete Volume}},
  booktitle =	{30th International Conference on Types for Proofs and Programs (TYPES 2024)},
  pages =	{1--190},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-376-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{336},
  editor =	{M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024},
  URN =		{urn:nbn:de:0030-drops-237954},
  doi =		{10.4230/LIPIcs.TYPES.2024},
  annote =	{Keywords: LIPIcs, Volume 336, TYPES 2024, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TYPES.2024.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Rasmus Ejlers Møgelberg and Benno van den Berg

Published in: LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{mogelberg_et_al:LIPIcs.TYPES.2024.0,
  author =	{M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{30th International Conference on Types for Proofs and Programs (TYPES 2024)},
  pages =	{0:i--0:xii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-376-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{336},
  editor =	{M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.0},
  URN =		{urn:nbn:de:0030-drops-237837},
  doi =		{10.4230/LIPIcs.TYPES.2024.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.CSL.2024.39
What Monads Can and Cannot Do with a Bit of Extra Time

Authors: Rasmus Ejlers Møgelberg and Maaike Annebet Zwart

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
The delay monad provides a way to introduce general recursion in type theory. To write programs that use a wide range of computational effects directly in type theory, we need to combine the delay monad with the monads of these effects. Here we present a first systematic study of such combinations. We study both the coinductive delay monad and its guarded recursive cousin, giving concrete examples of combining these with well-known computational effects. We also provide general theorems stating which algebraic effects distribute over the delay monad, and which do not. Lastly, we salvage some of the impossible cases by considering distributive laws up to weak bisimilarity.
Cite as

Rasmus Ejlers Møgelberg and Maaike Annebet Zwart. What Monads Can and Cannot Do with a Bit of Extra Time. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 39:1-39:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{mgelberg_et_al:LIPIcs.CSL.2024.39,
  author =	{M{\o}gelberg, Rasmus Ejlers and Zwart, Maaike Annebet},
  title =	{{What Monads Can and Cannot Do with a Bit of Extra Time}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{39:1--39:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.39},
  URN =		{urn:nbn:de:0030-drops-196823},
  doi =		{10.4230/LIPIcs.CSL.2024.39},
  annote =	{Keywords: Delay Monad, Monad Compositions, Distributive Laws, Guarded Recursion, Type Theory}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.23
The Clocks They Are Adjunctions Denotational Semantics for Clocked Type Theory

Authors: Bassel Mannaa and Rasmus Ejlers Møgelberg

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning about advanced programming language features using an abstract form of step-indexing. CloTT has previously been shown to enjoy a number of syntactic properties including strong normalisation, canonicity and decidability of type checking. In this paper we present a denotational semantics for CloTT useful, e.g., for studying future extensions of CloTT with constructions such as path types. The main challenge for constructing this model is to model the notion of ticks used in CloTT for coinductive reasoning about coinductive types. We build on a category previously used to model guarded recursion, but in this category there is no object of ticks, so tick-assumptions in a context can not be modelled using standard tools. Instead we show how ticks can be modelled using adjoint functors, and how to model the tick constant using a semantic substitution.
Cite as

Bassel Mannaa and Rasmus Ejlers Møgelberg. The Clocks They Are Adjunctions Denotational Semantics for Clocked Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{mannaa_et_al:LIPIcs.FSCD.2018.23,
  author =	{Mannaa, Bassel and M{\o}gelberg, Rasmus Ejlers},
  title =	{{The Clocks They Are Adjunctions Denotational Semantics for Clocked Type Theory}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.23},
  URN =		{urn:nbn:de:0030-drops-91938},
  doi =		{10.4230/LIPIcs.FSCD.2018.23},
  annote =	{Keywords: Guarded type theory, Coinduction, Presheaf model, Clocked type theory, Dependent adjunction}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact