Programming news · January 2025
A new language makes stack-based computation fully reversible
Matteo Palazzo and Luca Roversi of the University of Turin present SCORE, a programming language for manipulating stacks and variables that is reversible from the ground up.
Standard recipes for making a model reversible stall when computational states become ambiguous and operations are only partial functions, but SCORE is built so that its stack operations are total bijections, meaning every term can be run cleanly both forward and backward. The authors use formal verification to certify these properties, which they argue is essential for studying the computational complexity of reversible systems.
Robust reversible language design underpins everything from energy-recovery hardware compilation to reversible debuggers, and handling the stack discipline rigorously closes a long-standing gap.