Isomorphic Interpreters from Logically Reversible Abstract Machines

In our previous work, we developed a reversible programming language and established that every computation in it is a (partial) isomorphism that is reversible and that preserves information. The language is founded on type isomorphisms that have a clear categorical semantics but that are awkward as a notation for writing actual programs, especially recursive ones. This paper remedies this aspect by presenting a systematic technique for …