Reversible Monadic Computing

Chris Heunen, Martti Karvonen

Research output: Contribution to journalArticlepeer-review

Abstract

We extend categorical semantics of monadic programming to reversible computing, by considering monoidal closed dagger categories: the dagger gives reversibility, whereas closure gives higher-order expressivity. We demonstrate that Frobenius monads model the appropriate notion of coherence between the dagger and closure by reinforcing Cayley's theorem; by proving that effectful computations (Kleisli morphisms) are reversible precisely when the monad is Frobenius; by characterizing the largest reversible subcategory of Eilenberg–Moore algebras; and by identifying the latter algebras as measurements in our leading example of quantum computing. Strong Frobenius monads are characterized internally by Frobenius monoids.
Original languageEnglish
Pages (from-to)217-237
Number of pages21
JournalElectronic Notes in Theoretical Computer Science
Volume319
DOIs
Publication statusPublished - Dec 2015

Fingerprint Dive into the research topics of 'Reversible Monadic Computing'. Together they form a unique fingerprint.

Cite this