79 citations · 142 across the 16 of their papers we have counts for
20 papers
Garlene: Guarded Recursion in Lean
Sergei Stepanenko, Patrick Bahr, Rasmus Ejlers Møgelberg
Extending the recursion principles of a formal system is an enticing but dangerous endeavour with a well-documented history of leading to consistency bugs. Nakano's guarded recursi…
Multi-clocked Guarded Recursion Beyond ω
Rasmus Ejlers Møgelberg
Type theories with multi-clocked guarded recursion provide a flexible framework for programming with coinductive types encoding productivity in types. Combining this with solutions…
Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability
Giorgio Bacci, Rasmus Ejlers Møgelberg
Quantitative logic reasons about the degree to which formulas are satisfied. This paper studies the fundamental reasoning principles of higher-order quantitative logic and their ap…
Modelling Recursion and Probabilistic Choice in Guarded Type Theory
Philipp Jan Andries Stassen, Rasmus Ejlers Møgelberg, Maaike Zwart +2
Constructive type theory combines logic and programming in one language. This is useful both for reasoning about programs written in type theory, as well as for reasoning about oth…
What Monads Can and Cannot Do with a Few Extra Pages
Rasmus Ejlers Møgelberg, Maaike Zwart
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 c…
Asynchronous Modal FRP
Patrick Bahr, Rasmus Ejlers Møgelberg
Over the past decade, a number of languages for functional reactive programming (FRP) have been suggested, which use modal types to ensure properties like causality, productivity a…
Two Guarded Recursive Powerdomains for Applicative Simulation
Rasmus Ejlers Møgelberg, Andrea Vezzosi
Clocked Cubical Type Theory is a new type theory combining the power of guarded recursion with univalence and higher inductive types (HITs). This type theory can be used as a metal…
Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks
Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, Andrea Vezzosi
Guarded recursion is a powerful modal approach to recursion that can be seen as an abstract form of step-indexing. It is currently used extensively in separation logic to model pro…
Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory
Bassel Mannaa, Rasmus Ejlers Møgelberg, Niccolò Veltri
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 ab…
Diamonds are not forever: Liveness in reactive programming with guarded recursion
Patrick Bahr, Christian Uldal Graulund, Rasmus Møgelberg
When designing languages for functional reactive programming (FRP) the main challenge is to provide the user with a simple, flexible interface for writing programs on a high level…
Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming without Space Leaks
Patrick Bahr, Christian Graulund, Rasmus Møgelberg
Functional reactive programming (FRP) is a paradigm for programming with signals and events, allowing the user to describe reactive programs on a high level of abstraction. For thi…
Bisimulation as path type for guarded recursive types
Rasmus Ejlers Møgelberg, Niccolò Veltri
In type theory, coinductive types are used to represent processes, and are thus crucial for the formal verification of non-terminating reactive programs in proof assistants based o…
The clocks they are adjunctions:Denotational semantics for Clocked Type Theory
Bassel Mannaa, Rasmus Ejlers Møgelberg
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 ab…
Denotational semantics for guarded dependent type theory
Aleš Bizjak, Rasmus Ejlers Møgelberg
We present a new model of Guarded Dependent Type Theory (GDTT), a type theory with guarded recursion and multiple clocks in which one can program with, and reason about coinductive…
Guarded Dependent Type Theory with Coinductive Types
Aleš Bizjak, Hans Bugge Grathwohl, Ranald Clouston +2
We present guarded dependent type theory, gDTT, an extensional dependent type theory with a `later' modality and clock quantifiers for programming and proving with guarded recursiv…
Linear usage of state
Rasmus Ejlers Møgelberg, Sam Staton
We investigate the phenomenon that "every monad is a linear state monad". We do this by studying a fully-complete state-passing translation from an impure call-by-value language to…
Linear-use CPS translations in the Enriched Effect Calculus
Jeff Egger, Rasmus Ejlers Møgelberg, Alex Simpson
The enriched effect calculus (EEC) is an extension of Moggi's computational metalanguage with a selection of primitives from linear logic. This paper explores the enriched effect c…
First steps in synthetic guarded domain theory: step-indexing in the topos of trees
Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer +1
We present the topos S of trees as a model of guarded recursion. We study the internal dependently-typed higher-order logic of S and show that S models two modal operators, on pred…
Relational Parametricity for Computational Effects
Rasmus Ejlers Møgelberg, Alex Simpson
According to Strachey, a polymorphic program is parametric if it applies a uniform algorithm independently of the type instantiations at which it is applied. The notion of relation…
Linear Abadi and Plotkin Logic
Lars Birkedal, Rasmus E. Møgelberg, Rasmus Lerchedahl Petersen
We present a formalization of a version of Abadi and Plotkin's logic for parametricity for a polymorphic dual intuitionistic/linear type theory with fixed points, and show, followi…