L4 reversible intermediate language supports reversible program compilation
The Reversible Intermediate Language L4, its Type System, and its Bidirectional Small-Step Semantics
Programming Languages
Summary
Reversible computing involves running programs both forward and backward to save energy or improve debugging. The authors present L4, a new programming language designed to be an intermediate step that helps compile reversible programs efficiently for reversible machines. L4 has a special type system that manages how data is used only once (linear types) and supports execution in both directions. The authors also define formal rules that precisely describe how programs run forward and backward in small steps.
What this means in practice
- •For compiler engineers: Build compilers that translate reversible programs into reversible machine instructions using L4 to manage reversible program states precisely.
- •For debugging tool developers: Create debugging tools that can execute programs backward step-by-step to help diagnose bugs in reversible software effectively.
A theory result. No direct application yet.
Authors
Torben Ægidius Mogensen
Abstract
L4 is a generic, reversible, linearly-typed, low-level language intended as an intermediate language for compiling reversible programming languages to reversible machines. L4 is intended to replace and generalise RSSA, a reversible SSA form. Inspiration is drawn from other low-level reversible languages such as HSSA. In this paper, we define L4 first informally, and then give a formal type system and a bidirectional small-step semantics for L4: The rules have direction indicators to determine forwards or backwards execution, and the direction can be changed during execution.