Reversible Effects as Inverse Arrows

Research output: Contribution to journal › Conference article › Research › peer-review

Standard

Reversible Effects as Inverse Arrows. / Heunen, Chris; Kaarsgaard, Robin; Karvonen, Martti.

In: Electronic Notes in Theoretical Computer Science, Vol. 341, 01.12.2018, p. 179-199.

Research output: Contribution to journal › Conference article › Research › peer-review

Harvard

Heunen, C, Kaarsgaard, R & Karvonen, M 2018, 'Reversible Effects as Inverse Arrows', Electronic Notes in Theoretical Computer Science, vol. 341, pp. 179-199. https://doi.org/10.1016/j.entcs.2018.11.009

APA

Heunen, C., Kaarsgaard, R., & Karvonen, M. (2018). Reversible Effects as Inverse Arrows. Electronic Notes in Theoretical Computer Science, 341, 179-199. https://doi.org/10.1016/j.entcs.2018.11.009

Vancouver

Heunen C, Kaarsgaard R, Karvonen M. Reversible Effects as Inverse Arrows. Electronic Notes in Theoretical Computer Science. 2018 Dec 1;341:179-199. https://doi.org/10.1016/j.entcs.2018.11.009

Author

Heunen, Chris ; Kaarsgaard, Robin ; Karvonen, Martti. / Reversible Effects as Inverse Arrows. In: Electronic Notes in Theoretical Computer Science. 2018 ; Vol. 341. pp. 179-199.

Bibtex

@inproceedings{4df5fb2916c34c37b13bb772b1ae7ccf,
title = "Reversible Effects as Inverse Arrows",
abstract = "Reversible computing models settings in which all processes can be reversed. Applications include low-power computing, quantum computing, and robotics. It is unclear how to represent side-effects in this setting, because conventional methods need not respect reversibility. We model reversible effects by adapting Hughes' arrows to dagger arrows and inverse arrows. This captures several fundamental reversible effects, including serialization and mutable store computations. Whereas arrows are monoids in the category of profunctors, dagger arrows are involutive monoids in the category of profunctors, and inverse arrows satisfy certain additional properties. These semantics inform the design of functional reversible programs supporting side-effects.",
keywords = "Arrow, Inverse Category, Involutive Monoid, Reversible Effect",
author = "Chris Heunen and Robin Kaarsgaard and Martti Karvonen",
year = "2018",
month = dec,
day = "1",
doi = "10.1016/j.entcs.2018.11.009",
language = "English",
volume = "341",
pages = "179--199",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
note = "34th Conference on the Mathematical Foundations of Programming Semantics, MFPS ; Conference date: 06-06-2018 Through 09-06-2018",
url = "https://www.mathstat.dal.ca/mfps2018/",

}

RIS

TY - GEN

T1 - Reversible Effects as Inverse Arrows

AU - Heunen, Chris

AU - Kaarsgaard, Robin

AU - Karvonen, Martti

N1 - Conference code: 34

PY - 2018/12/1

Y1 - 2018/12/1

N2 - Reversible computing models settings in which all processes can be reversed. Applications include low-power computing, quantum computing, and robotics. It is unclear how to represent side-effects in this setting, because conventional methods need not respect reversibility. We model reversible effects by adapting Hughes' arrows to dagger arrows and inverse arrows. This captures several fundamental reversible effects, including serialization and mutable store computations. Whereas arrows are monoids in the category of profunctors, dagger arrows are involutive monoids in the category of profunctors, and inverse arrows satisfy certain additional properties. These semantics inform the design of functional reversible programs supporting side-effects.

AB - Reversible computing models settings in which all processes can be reversed. Applications include low-power computing, quantum computing, and robotics. It is unclear how to represent side-effects in this setting, because conventional methods need not respect reversibility. We model reversible effects by adapting Hughes' arrows to dagger arrows and inverse arrows. This captures several fundamental reversible effects, including serialization and mutable store computations. Whereas arrows are monoids in the category of profunctors, dagger arrows are involutive monoids in the category of profunctors, and inverse arrows satisfy certain additional properties. These semantics inform the design of functional reversible programs supporting side-effects.

KW - Arrow

KW - Inverse Category

KW - Involutive Monoid

KW - Reversible Effect

UR - http://www.scopus.com/inward/record.url?scp=85058019859&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2018.11.009

DO - 10.1016/j.entcs.2018.11.009

M3 - Conference article

VL - 341

SP - 179

EP - 199

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

T2 - 34th Conference on the Mathematical Foundations of Programming Semantics

Y2 - 6 June 2018 through 9 June 2018

ER -

ID: 211215598