PhD defence by Robin Kaarsgaard: The Logic of Reversible Computing - Theory and Practice


The Logic of Reversible Computing - Theory and Practice


Reversible computing is the study of models of computation that exhibit both forward and backward determinism. While reversible computing initially gained interest through its potential to reduce the energy consumption of computing machinery, via a result from physics now known as Landauer’s principle, a number of other applications in computer science have since been proposed, from syntax descriptions to model-based testing, debugging, and even robotics.

In spite of its numerous current (and potential future) applications, the established foundations for computation and programming, such as Turing machines, λ-calculi, and various categorical models, are largely ill equipped to handle reversible computing, as these often tacitly rely on irreversible operations to function. To set reversible computing on a foundation as solid as the one for conventional computing requires both a significant adaptation of existing techniques and the development of new ones.

In this thesis, we investigate reversible computing from a perspective of logic, broadly construed. To complement the operational point of view from which reversible computing is often studied, we offer a denotational account of reversibility in computation based on recent work in category theory. We propose two new techniques, founded in formal logic, for reasoning about reversible logic circuits. Further, we account for the behaviour of fixed points in certain proposed categorical models of reversible computing, and connect these results to the behaviour of recursive functions and data types in established reversible programming languages. In an application and extension of some of these results, we propose a uniform categorical foundation for a large class of reversible imperative programming languages known as structured reversible flowchart languages. We investigate the role of reversible effects in reversible functional programming, and show that a wide palette of these may be modelled as arrows (in the sense of Hughes) satisfying certain additional equations. Finally, we propose a brief vision for the future of the reversible functional programming language Rfun.

Assessment Committee

  • Chairman: Professor Friedrich Henglein, Department of Computer Science, University of Copenhagen, Denmark
  • Professor Robin Cockett, University of Calgary, Canada
  • Lead Research Scientist Tarmo Uustalu, Talinn University of Technology, Estland

Academic Supervisor & Co-Supervisors

  • Associate Professor Robert Glück, Department of Computer Science, University of Copenhagen
  • Co-Supervisor: Holger Bock Axelsen, Edlund A/S

For an electronic copy of the thesis, please contact