79 citations · 142 across the 16 of their papers we have counts for
Showing 2018Show all
3 papers · 1 filter
cs.LO2018
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…
cs.LO2018★ 4 cited
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…
cs.LO2018
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…