Search

• < Previous
• 1
• Next >

---

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 a new linear type theory: the enriched call-by-value calculus. The results are not specific to store, but can be&nbsp;[&hellip;]

---

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 calculus as a target language for continuation-passing-style (CPS) translations in which the typing of the translations&nbsp;[&hellip;]

---

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.

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 predicates and types, which serve as guards in recursive definitions of terms, predicates, and types. In particular, we show&nbsp;[&hellip;]

---

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 relational parametricity, introduced by Reynolds, is one possible mathematical formulation of this idea. Relational&nbsp;[&hellip;]

---

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 about advanced programming language features using an abstract form of step-indexing. CloTT has previously been shown to&nbsp;[&hellip;]

---