A reversible abstract machine architecture and its reversible machine code are presented and formalized. For machine code to be reversible, both the underlying control logic and each instruction must be reversible. A general class of machine instruction sets is proven to be reversible, building on our concept of reversible updates. The presentation is abstract and can serve as a guideline for a family of reversible processor designs. By example, we illustrate programming principles for the reversible abstract machine architecture formalized in this work.

Joint work with Holger Bock Axelsen (U Copenhagen) and Tetsuo Yokoyama (U Nagoya).