The Reversible Intermediate Language L4, its Type System, and its Bidirectional Small-Step Semantics
Overview & Synopsis
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.
Indexed from repository: arXiv
(
arxiv.org)
Keyboard Shortcuts:
← / → for pages • + / - for zoom • 0 to fit width
Powered by Mozilla PDF.js v3.11
Document Information
| Document Title | The Reversible Intermediate Language L4, its Type System, and its Bidirectional Small-Step Semantics |
|---|---|
| Author / Organization | Torben Ægidius Mogensen |
| Subject & Discipline | cs.PL |
| Categories | Science & Mathematics |
| Publication Year | 2026 |
| License / Rights | arXiv Open Access / Creative Commons |
| Resource Verification | Listed PDF (Verification Pending) |
| Original Host Website |
arXiv
(arxiv.org)
|
| File Format | application/pdf (Portable Document Format) |
| Language | EN |
| Catalog ID | DOC-264258 |
| Original Source Link | Visit Source Page on arxiv.org » |