Property-based testing offers program validation by generating random inputs to validate behavioural program properties. However, manually writing test-input generators remains a high barrier to adoption in industrial settings. This paper introduces pun, a proof-of-concept programming language that supports property-based testing natively. pun aims to generate inputs automatically based on inverse interpretation of its typing judgement rules. This approach significantly lowers the barrier of entry, but our evaluation shows that it unfortunately can also lower the quality of the generated inputs. The main reason for this quality decrease, is that arbitrarily chosen inputs rarely satisfy any pre-conditions that properties may require. However, the inputs do not need to be completely arbitrary and the quality of the generated inputs can be improved by applying non-deterministic inverse interpretation of the property that the test is trying to falsify. We outline in this paper how this approach can be a first step to make manually writing input-generators unnecessary in property-based testing.
Reversible programming languages aim to guarantee that every user-defined function can be inverted automatically, typically by imposing syntactic or typing restrictions. Existing high-level languages often trade usability for reversibility: for example, they may lack algebraic data types, provide nonstandard pattern matching, or require explicit type annotations. We present PisoLang, a user-oriented reversible functional language that extends the reversible core calculus of Chardonnet et al. [2] with a surface syntax with fewer restrictions, algebraic data types with constructors, and Hindley–Milner style type inference. PisoLang supports inductive types and higher-order functions, and permits controlled non-linear use of variables (including repeated variables in patterns) while preserving injectivity of pattern matching. We describe the core language with typing and evaluation rules, develop a type inference algorithm for it, and present a desugaring procedure that elaborates nested applications into an invertible let-normal form. We show expressiveness via case studies including arithmetic, polymorphic list processing, and run-length compression.
Energy constraints increasingly dominate modern processor and high-performance computing system design. Contemporary superscalar and out-of-order (OoO) processors achieve performance through mechanisms that rely on destructive state transitions, including register overwrites, speculative flushing, and memory updates. Reversible computation provides a theoretical pathway toward reducing energy dissipation associated with information destruction, yet prior work has largely remained confined to circuit-level implementations and isolated architectural prototypes. This work explores a framework for Fully Adiabatic, Reversible, and Superscalar (FARS) microarchitectures that reinterpret modern performance-oriented processor structures under reversible execution constraints. We are working to complete a microarchitectural research platform that we are developing to investigate how key high-performance mechanisms can be reformulated to preserve invertibility. As a concrete artifact, we have implemented and evaluated reversible branch predictors, demonstrating that complex speculative microarchitectural structures can be expressed as bijective state transitions. This provides quantitative insight into the storage and coordination overheads required for reversible scheduling mechanisms and establishes a foundation for extending reversibility to additional superscalar structures. This work-in-progress identifies architectural gaps to be filled and presents an example of an implemented reversible microarchitectural component as a step toward thermodynamically aware high-performance processor design.
Reversibility in the higher-order process calculus ρπ relies on tracking causal dependencies between processes and their (causal) ancestors. This bookkeeping introduces extra complexity to the calculus both syntactically—through the use of tags—and semantically, via additional structural congruence rules to manage them. Although this additional complexity is not a problem for the familiar reader, it creates a steep learning curve for newcomers. To soften this learning curve, we present a graph rewriting-based semantics for ρπ . We also present an implementation of this graph-based approach with a step-by-step interface, allowing one to familiarize quickly with concepts and intuitions of ρπ in a graphical and user-friendly way.
Petri nets constitute a foundational model of concurrency, which makes their reversible counterparts particularly relevant. Reversible Petri nets have been used to investigate the relationships between different models of concurrency, such as process calculi and event structures. In this paper, we address the problem of mechanizing the theory of reversible Petri nets with causally consistent reversibility. Specifically, we present a full mechanization of reversible Occurrence Petri nets in the Lean proof assistant. We formally verify that this model satisfies causal-dependent reversibility by mechanizing the so-called parabolic lemma.
Variational approaches to Quantum State Preparation (QSP) allow for low-depth and structured circuit ansatz, at the cost of non-convex optimization landscapes and barren plateaus that severely limit scalability. In contrast, exact synthesis methods typically involve exponential growth in the number of independent parameters, leading to a rapid increase in circuit depth. In this work, it is shown that the algebraic properties of the Standard Recursive Block Basis (SRBB) can partially overcome this delicate trade-off. By exploiting the algebraic structure of the SRBB decomposition and the CNOT-optimized circuit for its diagonal component, an exact parameter-solving procedure for the variational SRBB-based QSP problem is defined by analytically inverting the foundational parametric Lie map. As a consequence, a variationally trained circuit is converted to an exact one without increasing circuit depth or gate count. The resulting framework preserves the expressive power of the variational ansatz, thanks to the completeness of the SRBB, while eliminating optimization-induced limitations, shifting the computational problem entirely to a classical precomputation stage. The new exact QSP algorithm has been implemented via the PennyLane library and tested in HPC simulations (up to 12 qubits) to demonstrate the scalability of the parametric map resulting from the recursive structure of the diagonal component of SRBB. In this new exact framework, circuit design (and hence rotation parameters) is twinned with the Unitary Group Hermitian generators and their properties, opening up new optimization possibilities.
This tool demonstration presents PEARL, a partial evaluator for the reversible programming language ARL, along with its associated tools. Partial evaluation is a program optimization technique that specializes a program with respect to known inputs, typically producing more efficient programs. ARL is a reversible flowchart language based on pattern matching and dynamic data structures, making it well suited for symbolic manipulation. The demonstration shows how PEARL translates a reversible combinational circuit into an executable ARL simulation by specializing an interpreter for the circuit description language. The example is presented in full and illustrates how reversible languages can be prototyped using reversible interpreters. Currently, PEARL is the only freely available partial evaluator for a reversible programming language. It has also served as a foundation for novel experiments with inversion and partial evaluation.
Verification and simulation are critical components of the semiconductor design process. For challenging design components, the use of machine-checkable formal proofs offers a high level of confidence in correct function. In this work, our primary contribution is a formal adiabatic transition relation on discrete transistor network states, described in text and encoded in the Lean 4 language for machine-checked theorem proving. As a test case for this formal verification approach, we present a discrete adiabatic simulation algorithm motivated by the transition relation. We provide detailed proofs in both text and Lean 4 that our algorithmic approach generates the unique successor state as constrained by the transition relation, or reports that no adiabatic successor state exists.
This paper investigates reversible operational semantics for R-CORE, a minimal reversible core language that is r-Turing complete. While small-step semantics for reversible languages such as Janus have been previously explored, this work revisits the approach for R-CORE with a specific emphasis on local injectivity of individual inference rules and reversibility at the meta level. Building on the denotational semantics, we define a syntax-based small-step semantics in which control flow is made explicit through the use of a control token. Each inference rule is formulated as a partial injective function, thereby guaranteeing deterministic execution in both the forward and backward directions at the level of individual steps. To bridge structured syntax with reversible control flow, we introduce a finer-grained small-step semantics that decomposes commands into atomic flowchart operations, including steps, tests, and assertions. This formulation follows the reversible flowchart model and clarifies how global reversibility emerges from locally reversible control transfers. It provides a useful semantic perspective for studying reversible execution mechanisms across different reversible languages and systems, including reversible interpreters and reversible debuggers.
Whilst compiler techniques are well-known for a wide range of paradigms in conventional programming languages, compilers for reversible languages remain rare and are predominantly limited to the functional and procedural paradigms. In this paper we present our work on a translation from the reversible object-oriented programming language Roopl++ to the hybrid intermediate language HSSA. Our contributions are as follows: This paper provides a translation scheme for all language constructs of Roopl++, as well as a description of the implementation of dynamic memory in HSSA. Runtime error scenarios of Roopl++ are discussed and classified based on whether they need to be explicitly checked at runtime, or whether they manifest naturally as reversibility violations in the generated code. An overview of the techniques used to implement the compiler is given. Finally, we show that HSSA, with its concise kernel and extensible set of primitives, is well-suited as a reversible compilation target, and that introducing HSSA as an intermediate layer enables retargetable compilation, allowing the same Roopl++ frontend to be reused across multiple reversible backends.
In the context of CCSK, a reversible extension of CCS, we study different notions of bisimilarity (strong/weak, forward-only/reversible) and highlight their differences and commonalities. In particular, for the weak reversible case, not previously studied in the literature, we propose two variants, dubbed directional and mixed bisimilarity, depending on whether τ actions should be in the same direction (forward/backward) as the action being matched or not. We show, in particular, that mixed bisimilarity is a congruence and completely abstracts away from τ actions.
Processes in Erlang interact asynchronously through message passing via a mailbox. Specifying the timing of message receipt helps ensure the system’s correct behaviour, which depends on message delivery. A process may alter its behaviour if no message is received in the mailbox within a specified time interval. CauDEr is a reversible debugger grounded in Erlang’s reversible semantics. CauDEr supports causal-consistent reversible debugging for concurrent Erlang programs. However, CauDEr does not account for the causal nature of time passage; instead, it treats time solely as a value. This work introduces discrete time passage into the reversible semantics of Erlang, enabling timeout operations in receive actions as expected. A formal description of the time tick is incorporated into the reversible semantics of CauDEr. Finally, an implementation of our time passage in CauDEr is presented under the maximal progress assumption.
We introduce a reversible deep learning model for ^13 C Nuclear Magnetic Resonance (NMR) spectroscopy that uses a single conditional invertible neural network for both directions between molecular structures and spectra. The network is built from i-RevNet style bijective blocks, so the forward map and its inverse are available by construction. We train the model to predict a 128-bit binned spectrum code from a graph-based structure encoding, while the remaining latent dimensions capture residual variability. At inference time, we invert the same trained network to generate structure candidates from a spectrum code, which explicitly represents the one-to-many nature of spectrum-to-structure inference. On a filtered subset, the model is numerically invertible on trained examples, achieves spectrum-code prediction above chance, and produces coarse but meaningful structural signals when inverted on validation spectra. These results demonstrate that invertible architectures can unify spectrum prediction and uncertainty-aware candidate generation within one end-to-end model.
Quantum computing has attracted meaningful interest in recent years due to rapid advancements in applications such as optimization, cryptography, and machine learning. However, the successful implementation of quantum algorithms on real quantum hardware requires selecting the most suitable device via detailed performance evaluation, which is both time- and cost-intensive. This article proposes an automated framework to estimate the Probability of Success per Trial (PST) of executing quantum circuits on specific quantum devices. The approach involves constructing a dataset involving more than 4000 quantum circuits from the MQT Bench set. These circuits are then converted into Directed Acyclic Graph (DAG) representations, and Graph Neural Network (GNN)-based models are trained to predict the optimal associated PST for a target device, avoiding a brute-force exploration based on compiling and executing the quantum circuit, varying the compilation setting. The trained models have achieved good accuracy in estimating the PST value, guaranteeing a Root Mean Squared Error (RMSE) lower than 0.1 for all three target devices considered, significantly reducing the time and cost required for estimating the metric and proving the effectiveness of the proposed methodology.
Landauer's embeddings enable the reversibility of computations for non-reversible programming languages, augmenting each intermediate state with enough data to reconstruct the previous state. An interesting research question is therefore to try to reduce the space overhead required. In this work we propose a Landauer's embedding for Plotkin's call-by-value calculus (CbV). In order to control the computational complexity of CbV and turn the number of β-steps into a cost model, CbV is typically implemented via reduction machines. We show that one machine, that has not received much attention, exhibits a particularly compact Landauer's embedding, requiring only constant space overhead for each step.
The AND gate is not reversible—on qubits. However, it is reversible on qutrits, making it a building block for efficient simulation of qubit computation using qutrits. We first observe that there are multiple two-qutrit Clifford+T unitaries that realize the AND gate with T-count 3, and its generalizations to n qubits with T-count 3n-3 . Our main result is the construction of a novel qutrit [[6, 2, 2]] quantum error-correcting code with a transversal implementation of the AND gate. The key insight in our approach is that a symmetric T-depth one circuit decomposition—composed of a CX circuit, T and T dagger gates, followed by the CX circuit in reverse—of a given unitary can be interpreted as a CSS code. We can increase the code distance by augmenting the code circuit with additional stabilizers while preserving the logical gate. This results in a code with a “built-in” transversal implementation of the original unitary, which can be further concatenated to attain a [[48,2,4 ]] code with the same transversal logical gate. Furthermore, we present several protocols for mixed qubit-qutrit codes which we call Qubit Subspace Codes, and for magic state distillation and injection.
Janus is a paradigmatic example of a reversible programming language. Indeed, Janus programs can be executed backwards as well as forwards. However, its current small-step semantics (useful, e.g., for debugging or as a basis for extensions with concurrency primitives) is not reversible, since it discards information while computing forwards. For instance, it does not satisfy the so-called Loop Lemma, stating that any reduction has an inverse, a main property of reversibility in process calculi, where a small-step semantics is commonly used. We present in this paper a novel small-step semantics which is actually reversible (for well-formed Janus programs), while remaining equivalent to the previous one. In particular, this involves the non-trivial challenge of defining a semantics based on a “program counter” for a high-level programming language.
Reversible process calculi, such as 𝚛𝚘𝚕𝚕-π , can accommodate fault-tolerant communication protocols. However, untyped process calculi cannot guarantee desirable behavioural properties such as deadlock-freedom. Concomitantly, Multiparty Session Types (MPST) can provide such guarantees by construction, but often do not consider failures. This suggests that, by leveraging both MPST and 𝚛𝚘𝚕𝚕-π , we can facilitate the representation of failures without requiring a significant extension to the MPST theory. However, 𝚛𝚘𝚕𝚕-π lacks choice and replication primitives, which are key features for an MPST-based type system. Nonetheless, its expressiveness allows these constructs to be encoded directly. In this paper, we introduce 𝚛𝚘𝚕𝚕-π !⊕ , a variant of 𝚛𝚘𝚕𝚕-π that incorporates choice and replication, and outline its encoding in 𝚛𝚘𝚕𝚕-π . This extension lays the foundation for integrating 𝚛𝚘𝚕𝚕-π with MPST.
In quantum computing, graph states play a crucial role in quantum error correction and measurement-based quantum computing. Preparing these states efficiently on hardware with constrained connectivity is a fundamental challenge. In this work, we establish a universal framework for graph state preparation using only Controlled-Z (CZ) gates along the edges of a given hardware connectivity graph and local complementation operations. We prove that any graph state can be prepared using only these operations, providing a constructive transpilation method that transforms the input circuit into an equivalent one without increasing the number of entangling gates. Additionally, as our approach preserves entangling count and depth of the input circuit, we show that this framework also allows for optimal graph state preparation.
Quantum state preparation is a fundamental subroutine for many quantum algorithms, including linear system solvers, algorithms for Hamiltonian simulation, and quantum machine learning. Quantum state preparation consists in preparing an n-qubit quantum state through the definition of a unitary matrix that acts on the quantum register, conventionally initialized with all qubits in the zero state. Despite the transversal relevance, the characterization of its circuit depth complexity remained an open problem until the work by Sun et al., which discovered the asymptotically optimal space-time trade-off bounds when m ancillary qubits are available. Additionally, their algorithm resolves the depth complexity for circuits without ancillary qubits. In this work, a first implementation of the optimally bounded algorithm by Sun et al. is presented, framed in the parametric range m = 2n and using the PennyLane library. A novel strategy for handling the complete set of parameters of the general complex case is presented from a theoretical point of view and tested to establish its effectiveness. To assess the scalability of the implemented algorithm, several quantum states have been prepared in simulation up to 8 qubits, both dense and sparse, including states of specific interest such as Bell or GHZ states.
