Search

• < Previous
• 1
• Next >

---

Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory

Mathys Rennela ; Sam Staton.

We describe categorical models of a circuit-based (quantum) functional programming language. We show that enriched categories play a crucial role. Following earlier work on QWire by Paykin et al., we consider both a simple first-order linear language for circuits, and a more powerful host language,&nbsp;[&hellip;]

---

Higher Order Automatic Differentiation of Higher Order Functions

Mathieu Huot ; Sam Staton ; Matthijs Vákár.

We present semantic correctness proofs of automatic differentiation (AD). We consider a forward-mode AD method on a higher order language with algebraic data types, and we characterise it as the unique structure preserving macro given a choice of derivatives for basic operations. We describe a rich&nbsp;[&hellip;]

---

Relating coalgebraic notions of bisimulation

Sam Staton.

The theory of coalgebras, for an endofunctor on a category, has been proposed as a general theory of transition systems. We investigate and relate four generalizations of bisimulation to this setting, providing conditions under which the four different generalizations coincide. We study transfinite&nbsp;[&hellip;]

---

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;]

---