Modern programming languages and operating systems use heap memory
that allows allocation and deallocation of memory to be decoupled, so
they don't follow a stack discipline. Axelsen and Glück have
presented a reversible heap manager where allocation and deallocation
are each other's logical inverses: Freeing a block of memory is done
by running the allocation procedure backwards.

Axelsen and Glück use this heap manager to sketch implementation of a
simple reversible functional language where pattern matching a
constructor is the inverse of construction, so pattern-matching
implies deallocation. This requires the language to be linear: A
pointer can not be copied and it can only be eliminated by
deallocating the node to which it points.

We overcome this limitation by adding reference counts to nodes:
Copying a pointer to a node increases the reference count of the node
and eliminating a pointer decreases the reference count. We show
reversible implementations of operations on nodes with reference
counts. We then show these operations can be used when implementing a
reversible functional language RCFUN to the reversible imperative
language Janus.