1. 1

Abstract: Computation is a physical process which, like all other physical processes, is fundamentally reversible. From the notion of type isomorphisms, we derive a typed, universal, and reversible computational model in which information is treated as a linear resource that can neither be duplicated nor erased. We use this model as a semantic foundation for computation and show that the “gap” between conventional irreversible computation and logically reversible computation can be captured by a type-and-effect system. Our type-and-effect system is structured as an arrow metalanguage that exposes creation and erasure of information as explicit effect operations. Irreversible computations arise from interactions with an implicit information environment, thus making them a derived notion, much like open systems in Physics. We sketch several applications which can benefit from an explicit treatment of information effects, such as quantitative information-flow security and differential privacy.


  2. 1

    It seems to me that this paper has a confusing title. It gives a very nice construction on top of universal reversible gates to construct a combinatorial system that expresses the notion of reversibility for three types: unit, sum, product.

    Actually, the first author has collected all its work into a PhD thesis, which includes an even more useful result: to model subtraction types (dual of sum types) for modelling coroutines, and fractional types (dual of product types) for modelling concurrency or constraint solving.

    If someone is interested, I could post a link to this secondary paper that uses the results of reversible computing to define these fascinating types.