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.
