https://arxiv.org/api/0lw0omWKvp4CXpbkk0N5nFWpqWg 2026-06-22T02:44:37Z 9918 885 15 http://arxiv.org/abs/2507.15530v2 2025-12-01T22:14:19Z

Bayesian probabilistic programming languages (BPPLs) let users denote statistical models as code while the interpreter infers the posterior distribution. The semantics of BPPLs are usually mathematically complex and unable to reason about desirable properties such as expected values and independence of random variables. To reason about these properties in a non-Bayesian setting, probabilistic separation logics such as PSL and Lilac interpret separating conjunction as probabilistic independence of random variables. However, no existing separation logic can handle Bayesian updating, which is the key distinguishing feature of BPPLs. To close this gap, we introduce Bayesian separation logic (BaSL), a probabilistic separation logic that gives semantics to BPPL. We prove an internal version of Bayes' theorem using a result in measure theory known as the Rokhlin-Simmons disintegration theorem. Consequently, BaSL can model probabilistic programming concepts such as Bayesian updating, unnormalised distribution, conditional distribution, soft constraint, conjugate prior and improper prior while maintaining modularity via the frame rule. The model of BaSL is based on a novel instantiation of Kripke resource monoid via $σ$-finite measure spaces over the Hilbert cube, and the semantics of Hoare triple is compatible with an existing denotational semantics of BPPL based on the category of $s$-finite kernels. Using BaSL, we then prove properties of statistical models such as the expected value of Bayesian coin flip, correlation of random variables in the collider Bayesian network, the posterior distributions of the burglar alarm model, a parameter estimation algorithm, and the Gaussian mixture model.

2025-07-21T11:56:11Z Accepted to POPL 2026; Extended version with proofs Shing Hin Ho Nicolas Wu Azalea Raad http://arxiv.org/abs/2507.11676v2 2025-12-01T16:26:39Z

Quantum programs today are written at a low level of abstraction - quantum circuits akin to assembly languages - and the unitary parts of even advanced quantum programming languages essentially function as circuit description languages. This state of affairs impedes scalability, clarity, and support for higher-level reasoning. More abstract and expressive quantum programming constructs are needed. To this end, we introduce a simple syntax for generating unitaries from "just a phase"; we combine a (global) phase operation that captures phase shifts with a quantum analogue of the "if let" construct that captures subspace selection via pattern matching. This minimal language lifts the focus from gates to eigendecomposition, conjugation, and controlled unitaries; common building blocks in quantum algorithm design. We demonstrate several aspects of the expressive power of our language in several ways. Firstly, we establish that our representation is universal by deriving a universal quantum gate set. Secondly, we show that important quantum algorithms can be expressed naturally and concisely, including Grover's search algorithm, Hamiltonian simulation, Quantum Fourier Transform, Quantum Signal Processing, and the Quantum Eigenvalue Transformation. Furthermore, we give clean denotational semantics grounded in categorical quantum mechanics. Finally, we implement a prototype compiler that efficiently translates terms of our language to quantum circuits, and prove that it is sound with respect to these semantics. Collectively, these contributions show that this construct offers a principled and practical step toward more abstract and structured quantum programming.

2025-07-15T19:31:53Z 42 pages, 5 figures Chris Heunen Louis Lemonnier Christopher McNally Alex Rice 10.1145/3776731 http://arxiv.org/abs/2505.05162v2 2025-12-01T11:11:23Z

A key computational question underpinning the automated testing and verification of concurrent programs is the consistency question - given a partial execution history, can it be completed in a consistent manner? Due to its importance, consistency testing has been studied extensively for memory models, as well as for database isolation levels. A common theme in all these settings is the use of shared-memory as the primal mode of interthread communication. On the other hand, modern programming languages, such as Go, Rust and Kotlin, advocate a paradigm shift towards channel-based (i.e., message-passing) communication. However, the consistency question for channel-based concurrency is currently poorly understood. In this paper we lift the study of fundamental consistency problems to channels, taking into account various input parameters, such as the number of threads executing, the number of channels, and the channel capacities. We draw a rich complexity landscape, including upper bounds that become polynomial when certain input parameters are fixed, as well as hardness lower bounds. Our upper bounds are based on algorithms that can drive the verification of channel consistency in automated verification tools. Our lower bounds characterize minimal input parameters that are sufficient for hardness to arise, and thus shed light on the intricacies of testing channel-based concurrency. In combination, our upper and lower bounds characterize the boundary of tractability/intractability of verifying channel consistency, and imply that our algorithms are often (nearly) optimal.

2025-05-08T11:57:28Z Extended version of paper "The Complexity of Testing Message-Passing Concurrency" on POPL 2026 Zheng Shi Lasse Møldrup Umang Mathur Andreas Pavlogiannis http://arxiv.org/abs/2512.01036v1 2025-11-30T19:05:50Z

We describe an exact sampler for a simply-typed, first-order functional programming language. Given an acyclic finite automaton, $α_{\varnothing}$, it samples a random function uniformly without replacement from well-typed functions in $\mathcal{L}(α_{\varnothing})$. This is achieved via a fixed-parameter tractable reduction from a syntax-directed type system to a context-free grammar, preserving type soundness and completeness w.r.t. $\mathcal{L}(α_{\varnothing})$, while retaining the robust metatheory of formal languages.

2025-11-30T19:05:50Z 2 pages Breandan Considine http://arxiv.org/abs/2512.00487v1 2025-11-29T13:37:06Z

With the growing diversity of instruction set architectures (ISAs), cross-ISA program execution has become common. Dynamic binary translation (DBT) is the main solution but suffers from poor performance. Cross-compilation avoids emulation costs but is constrained by an "all-or-nothing" model-programs are either fully cross-compiled or entirely emulated. Complete cross-compilation is often unfeasible due to ISA-specific code or missing dependencies, leaving programs with high emulation overhead. We propose a hybrid execution system that combines compilation and emulation, featuring a selective function offloading mechanism. This mechanism establishes cross-environment calling channels, offloading eligible functions to the host for native execution to reduce DBT overhead. Key optimizations address offloading costs, enabling efficient hybrid operation. Built on LLVM and QEMU, the system works automatically for both applications and libraries. Evaluations show it achieves up to 13x speedups over existing DBT, with strong practical value.

2025-11-29T13:37:06Z Yuhao Gu Zhongchun Zheng Nong Xiao Yutong Lu Xianwei Zhang http://arxiv.org/abs/2512.00314v1 2025-11-29T04:28:27Z

In this work, we study the problems of counting and sampling Mazurkiewicz traces that a regular language touches. Fix an alphabet $Σ$ and an independence relation $\mathbb{I} \subseteq Σ\times Σ$. The input consists of a regular language $L \subseteq Σ^*$, given by a finite automaton with $m$ states, and a natural number $n$ (in unary). For the counting problem, the goal is to compute the number of Mazurkiewicz traces (induced by $\mathbb{I}$) that intersect the $n^\text{th}$ slice $L_n = L \cap Σ^n$, i.e., traces that admit at least one linearization in $L_n$. For the sampling problem, the goal is to output a trace drawn from a distribution that is approximately uniform over all such traces. These tasks are motivated by bounded model checking with partial-order reduction, where an \emph{a priori} estimate of the reduced state space is valuable, and by testing methods for concurrent programs that use partial-order-aware random exploration. We first show that the counting problem is #P-hard even when $L$ is accepted by a deterministic automaton, in sharp contrast to counting words of a DFA, which is polynomial-time solvable. We then prove that the problem lies in #P for both NFAs and DFAs, irrespective of whether $L$ is trace-closed. Our main algorithmic contributions are a \emph{fully polynomial-time randomized approximation scheme} (FPRAS) that, with high probability, approximates the desired count within a prescribed accuracy, and a \emph{fully polynomial-time almost uniform sampler} (FPAUS) that generates traces whose distribution is provably close to uniform.

2025-11-29T04:28:27Z To appear in POPL 2026. Author order is random Alexis de Colnet Kuldeep S. Meel Umang Mathur 10.1145/3776723 http://arxiv.org/abs/2404.04218v4 2025-11-28T18:37:48Z

Algebraic effect handlers are becoming an increasingly popular way of structuring effectful computations, and their performance is often a concern. One of the proposed approaches towards efficient compilation is tracking effect information through explicit subtyping coercions. However, in the presence of polymorphism, these coercions are compiled into additional arguments of compiled functions, incurring significant overhead. In this paper, we present a polymorphic effectful calculus, identify simplification phases needed to reduce the number of unnecessary constraints, and prove that they preserve semantics. In addition, we implement the simplification algorithm in the Eff language and evaluate its performance on a number of benchmarks. Though we do not prove the optimality of the presented simplifications, the results show that the algorithm eliminates all coercions, resulting in code as efficient as manually monomorphised one.

2024-04-05T17:04:17Z Logical Methods in Computer Science, Volume 21, Issue 4 (December 1, 2025) lmcs:13366 Filip Koprivec Matija Pretnar 10.46298/lmcs-21(4:25)2025 http://arxiv.org/abs/2512.03083v1 2025-11-28T18:05:54Z

Effect handlers are increasingly prominent in modern programming for managing complex computational effects, including concurrency, asynchronous operations, and exception handling, in a modular and flexible manner. Efficient stack management remains a significant challenge for effect handlers due to the dynamic control flow changes they introduce. This paper explores a novel stack management approach using user-level overcommitting within the libseff C library, which leverages virtual memory mechanisms and protection-based lazy allocation combined with signal-driven memory commitment. Our user-level overcommitting implementation dynamically resizes stacks on-demand, improving memory utilization and reducing waste compared to traditional methods. We rigorously benchmark and evaluate this novel strategy against conventional fixed-size stacks, segmented stacks, and kernel-based overcommitting, using metrics such as context-switch latency, stack expansion efficiency, multi-threaded performance, and robustness under rapid stack growth conditions. Experimental results demonstrate that kernel-based overcommitting achieves an effective balance between performance and flexibility, whereas our user-level implementation, while flexible, incurs additional overheads, highlighting areas for optimization. This study provides a detailed comparative analysis of various stack management strategies, offering practical recommendations tailored to specific application requirements and operational constraints. Future work will focus on refining user-level overcommitting mechanisms, mitigating non-deterministic behaviors, and expanding benchmark frameworks to include real-world scenarios.

2025-11-28T18:05:54Z ZeHao Yu http://arxiv.org/abs/2511.18531v2 2025-11-28T13:42:32Z

Despite rapid progress in logic locking (LL), reproducibility remains a challenge as codes are rarely made public. We present LockForge, a first-of-its-kind, multi-agent large language model (LLM) framework that turns LL descriptions in papers into executable and tested code. LockForge provides a carefully crafted pipeline realizing forethought, implementation, iterative refinement, and a multi-stage validation, all to systematically bridge the gap between prose and practice for complex LL schemes. For validation, we devise (i) an LLM-as-Judge stage with a scoring system considering behavioral checks, conceptual mechanisms, structural elements, and reproducibility on benchmarks, and (ii) an independent LLM-as-Examiner stage for ground-truth assessment. We apply LockForge to 10 seminal LL schemes, many of which lack reference implementations. Our evaluation on multiple SOTA LLMs, including ablation studies, reveals the significant complexity of the task. We show that an advanced reasoning model and a sophisticated, multi-stage framework like LockForge are required. We release all implementations and benchmarks, providing a reproducible and fair foundation for evaluation of further LL research.

2025-11-23T16:51:32Z Akashdeep Saha Zeng Wang Prithwish Basu Roy Johann Knechtel Ozgur Sinanoglu Ramesh Karri http://arxiv.org/abs/2503.20690v2 2025-11-28T13:37:13Z

Smart contracts are small programs that run autonomously on the blockchain, using it as their persistent memory. The predominant platform for smart contracts is the Ethereum VM (EVM). In EVM smart contracts, a problem with significant applications is to identify data structures (in blockchain state, a.k.a. "storage"), given only the deployed smart contract code. The problem has been highly challenging and has often been considered nearly impossible to address satisfactorily. (For reference, the latest state-of-the-art research tool fails to recover nearly all complex data structures and scales to under 50% of contracts.) Much of the complication is that the main on-chain data structures (mappings and arrays) have their locations derived dynamically through code execution. We propose sophisticated static analysis techniques to solve the identification of on-chain data structures with extremely high fidelity and completeness. Our analysis scales nearly universally and recovers deep data structures. Our techniques are able to identify the exact types of data structures with 98.6% precision and at least 92.6% recall, compared to a state-of-the-art tool managing 80.8% and 68.2% respectively. Strikingly, the analysis is often more complete than the storage description that the compiler itself produces, with full access to the source code.

2025-03-26T16:22:08Z Extended Version of ICSE 2026 paper Sifis Lagouvardos Yannis Bollanos Michael Debono Neville Grech Yannis Smaragdakis http://arxiv.org/abs/2511.22692v1 2025-11-27T18:48:27Z

Multiparty session types (MPST) provide a rigorous foundation for verifying the safety and liveness of concurrent systems. However, existing approaches often force a difficult trade-off: classical, projection-based techniques are compositional but limited in expressiveness, while more recent techniques achieve higher expressiveness by relying on non-compositional, whole-system model checking, which scales poorly. This paper introduces a new approach to MPST that delivers both expressiveness and compositionality, called the synthetic approach. Our key innovation is a type system that verifies each process directly against a global protocol specification, represented as a labelled transition system (LTS) in general, with global types as a special case. This approach uniquely avoids the need for intermediate local types and projection. We demonstrate that our approach, while conceptually simpler, supports a benchmark of challenging protocols that were previously beyond the reach of compositional techniques in the MPST literature. We generalise our type system, showing that it can validate processes against any specification that constitutes a "well-behaved" LTS, supporting protocols not expressible with the standard global type syntax. The entire framework, including all theorems and many examples, has been formalised and mechanised in Agda, and we have developed a prototype implementation as an extension to VS Code.

2025-11-27T18:48:27Z David Castro-Perez Francisco Ferreira Sung-Shik Jongmans http://arxiv.org/abs/2511.22537v1 2025-11-27T15:16:59Z

The two main notions of control in quantum programming languages are often referred to as "quantum" control and "classical" control. With the latter, the control flow is based on classical information, potentially resulting from a quantum measurement, and this paradigm is well-suited to mixed state quantum computation. Whereas with quantum control, we are primarily focused on pure quantum computation and there the "control" is based on superposition. The two paradigms have not mixed well traditionally and they are almost always treated separately. In this work, we show that the paradigms may be combined within the same system. The key ingredients for achieving this are: (1) syntactically: a modality for incorporating pure quantum types into a mixed state quantum type system; (2) operationally: an adaptation of the notion of "quantum configuration" from quantum lambda-calculi, where the quantum data is replaced with pure quantum primitives; (3) denotationally: suitable (sub)categories of Hilbert spaces, for pure computation and von Neumann algebras, for mixed state computation in the Heisenberg picture of quantum mechanics.

2025-11-27T15:16:59Z Extended version of https://www.doi.org/10.1007/978-3-031-90897-2_8 and related to the PhD thesis at arXiv:2406.07216 Kinnari Dave Louis Lemonnier Romain Péchoux Vladimir Zamdzhiev http://arxiv.org/abs/2511.22523v1 2025-11-27T15:03:46Z

Equivalence checking of hybrid quantum circuits is of primary importance, given that quantum circuit transformations are omnipresent along the quantum compiler chain. While some approaches exist for automating this task, most focus on the simple case of unitary circuits. At the same time, real quantum computing requires hybrid circuits equipped with measurement operators. Moreover, the few approaches targeting the hybrid case are limited to a restricted class of problems. We propose tackling the Quantum Hybrid Circuit Equivalence Checking problem through lifting unitary circuit verification using a transformation known as deferred measurement. We show that this approach alone significantly outperforms prior work, and that, with the addition of specific unitary-level techniques we call separation and projection, it can handle much larger classes of hybrid circuit equivalence problems. We have implemented and evaluated our method over standard circuit transformations such as teleportation, one-way measurement, or the IBM Qiskit compiler, demonstrating its promises. As a side finding, we have identified and reported several unexpected behaviours with the Qiskit compiler.

2025-11-27T15:03:46Z 16 pages, 5 figures, 3 tables Jérome Ricciardi Sébastien Bardin Christophe Chareton Benoît Valiron http://arxiv.org/abs/2511.22419v1 2025-11-27T12:57:46Z

In this paper, a monad-based denotational model is introduced and shown adequate for the Proto-Quipper family of calculi, themselves being idealized versions of the Quipper programming language. The use of a monadic approach allows us to separate the value to which a term reduces from the circuit that the term itself produces as a side effect. In turn, this enables the denotational interpretation and validation of rich type systems in which the size of the produced circuit can be controlled. Notably, the proposed semantic framework, through the novel concept of circuit algebra, suggests forms of effect typing guaranteeing quantitative properties about the resulting circuit, even in presence of optimizations.

2025-11-27T12:57:46Z Extended version of a paper to be published at POPL 2026 Ken Sakayori Andrea Colledan Ugo Dal Lago http://arxiv.org/abs/2501.16607v3 2025-11-27T09:37:42Z

Text-to-SQL is a fundamental yet challenging task in the NLP area, aiming at translating natural language questions into SQL queries. While recent advances in large language models have greatly improved performance, most existing approaches depend on models with tens of billions of parameters or costly APIs, limiting their applicability in resource-constrained environments. For real world, especially on edge devices, it is crucial for Text-to-SQL to ensure cost-effectiveness. Therefore, enabling the light-weight models for Text-to-SQL is of great practical significance. However, smaller LLMs often struggle with complicated user instruction, redundant schema linking or syntax correctness. To address these challenges, we propose MCTS-SQL, a novel framework that uses Monte Carlo Tree Search to guide SQL generation through multi-step refinement. Since the light-weight models' weak performance of single-shot prediction, we generate better results through several trials with feedback. However, directly applying MCTS-based methods inevitably leads to significant time and computational overhead. Driven by this issue, we propose a token-level prefix-cache mechanism that stores prior information during iterations, effectively improved the execution speed. Experiments results on the SPIDER and BIRD benchmarks demonstrate the effectiveness of our approach. Using a small open-source Qwen2.5-Coder-1.5B, our method outperforms ChatGPT-3.5. When leveraging a more powerful model Gemini 2.5 to explore the performance upper bound, we achieved results competitive with the SOTA. Our findings demonstrate that even small models can be effectively deployed in practical Text-to-SQL systems with the right strategy.

2025-01-28T00:52:23Z Accepted by AAAI 2026 Shuozhi Yuan Limin Chen Miaomiao Yuan Zhao Jin