Reversible execution

The ability to backtrack, or retrace, the execution of a computer program has gained wider acceptance recently as a desired feature within a programming language. This is particularly useful in two different applications: (1) In debugging systems where the trace output is saved and can be interrogated under programmer control [1, 3]; (2) In artificial intelligence applications where one is trying to prove a certain result. It is frequently necessary to backup the proof and try some alternative path [2].