4 papers
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…
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…
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…