Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.31201

The Reversible Intermediate Language L4, its Type System, and its Bidirectional Small-Step Semantics

Torben Ægidius Mogensen
View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

cs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Torben Ægidius Mogensen. 2026-10-22. The Reversible Intermediate Language L4, its Type System, and its Bidirectional Small-Step Semantics. https://arxiv.org/abs/2610.31201

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Structure-Aware Equivalence for Evaluating Autoformalized Statements

Evaluating autoformalized mathematical statements requires determining whether a candidate preserves the mathematical claim intended by a trusted reference. Existing methods approach this problem from complementary directions: reference-free learned evaluators estimate semantic agreement but are not constrained to a formal equivalence relation, while reference-based proof methods typically employ whole-statement logical equivalence to provide formal certificates, which is too coarse for translation fidelity and may identify mathematically unrelated statements. We introduce Structure-Aware Equivalence (SAE), a role-preserving formal equivalence relation between syntactic and whole-statement logical equivalence that allows formally justified reformulations while preserving translation-relevant mathematical structure. We operationalize SAE in the Autoformalization Correctness Evaluator (ACE), which provides certified equivalence or inequivalence judgments and reports Inconclusive otherwise. On ProofNetVerif, a benchmark introduced with BEq+, ACE retains substantial equivalent-case coverage while remaining highly conservative in certifying disputed or inequivalent pairs. On targeted diagnostics, BEq+ accepts 94-96% of unrelated but whole-statement logically equivalent pairs, while Mathesis LeanScorer accepts 42% of localized meaning-changing perturbations; ACE accepts none of either set as equivalent.

cs.PL↗
arXiv2026

Operon: Incremental Construction of Ragged Data via Named Dimensions

Modern data processing workflows frequently encounter ragged data: multidimensional collections whose inner lengths vary and are revealed only at runtime. Ragged data is prevalent in domains throughout science and computing, yet existing workflow engines treat it as nested containers. This representation leaves shape semantics ambiguous, obscures task dependencies when upstream coordinates are not yet enumerated, and imposes coarse synchronization barriers that stall independent work across tasks. We argue that ragged data is fundamentally a flat function over a coordinate space, and that making this view explicit resolves all three difficulties at once. We realize this insight in Operon, a statically verifiable workflow engine built around a formalism of named dimensions with explicit dependency relations. Users declare pipelines in the Operon DSL by annotating data flow with dimension names, where the static checker verifies that every task does not include faulty iterations regardless of runtime lengths. At runtime, the system models in-progress arrays as partial functions over downward-closed coordinate domains, which provides a natural representation for partially-unknown data states, an exact notion of per-task indegree before all upstream coordinates are enumerated, and a sound basis for fault recovery without programmer intervention.

cs.PL↗
arXiv2026

Multiobjective Preexpectation Reasoning for Probabilistic Programs

Probabilistic programs with nondeterminism model planning problems in which a strategy typically resolves the nondeterminism to meet a specification. We study the multiobjective setting, meeting several specifications at once along a Pareto front, and provide a deductive, program-level account of strategy synthesis. Its core is a multiobjective preexpectation transformer mapping a tuple of postexpectations to the set of simultaneously achievable values, an element of the convex Hoare powerdomain. It conservatively extends weakest preexpectations and lifts standard loop rules. We develop rules to synthesize witnessing strategies as mixed determinizations that solve nondeterminism probabilistically. We prove the transformer and synthesis rules sound against an operational Markov decision process (MDP) semantics, without requiring a finite state space: our approach can be seen as a symbolic approach - at program level - for multiobjective optimization over infinite MDPs. We demonstrate our machinery using two case studies.

cs.PL↗