https://arxiv.org/api/C7F5ysXTeylZFJmYEg3NK9haxe0 2026-03-22T10:09:01Z 9537 15 15 http://arxiv.org/abs/2603.17099v1 2026-03-17T19:39:56Z

Vectorization is a compiler optimization that replaces multiple operations on scalar values with a single operation on vector values. Although common in traditional compilers such as rustc, clang, and gcc, vectorization is not common in the Verilog ecosystem. This happens because, even though Verilog supports vector notation, the language provides no semantic guarantee that a vectorized signal behaves as a word-level entity: synthesis tools still resolve multiple individual assignments and a single vector assignment into the same set of parallel wire connections. However, vectorization brings important benefits in other domains. In particular, it reduces symbolic complexity even when the underlying hardware remains unchanged. Formal verification tools such as Cadence Jasper operates at the symbolic level: they reason about Boolean functions, state transitions, and equivalence classes, rather than about individual wires or gates. When these tools can treat a bus as a single symbolic entity, they scale more efficiently. This paper supports this observation by introducing a Verilog vectorizer. The vectorizer, built on top of the CIRCT compilation infrastructure, recognizes several vectorization patterns, including inverted assignments, assignments involving complex expressions, and inter-module assignments. It has been experimented with some Electronic design automation (EDA) tools, and for Jasper tool, it improves elaboration time by 28.12% and reduces memory consumption by 51.30% on 1,157 designs from the ChiBench collection.

2026-03-17T19:39:56Z 12 pages, 16 figures, 4 algorithms, 4 theorems Maria Fernanda Oiveira Guimarães Ulisses Rosa Ian Trudel João Victor Amorim Vieira Augusto Amaral Mafra Mirlaine Crepalde Fernando Magno Quintão Pereira http://arxiv.org/abs/2603.16650v1 2026-03-17T15:20:28Z

As spin-based quantum systems scale, their setup and control complexity increase sharply. In semiconductor quantum dot (QD) experiments, device-to-device variability, heterogeneous control-electronics stacks, and differing operational modalities make it difficult to reuse characterization, calibration, and control logic across laboratories. We present FAlCon, an open-source software ecosystem for portable, automated characterization and tuning measurement workflows. FAlCon provides (i) a lightweight domain-specific language for expressing state-based tuning logic in a hardware-agnostic form; (ii) specialized transmittable libraries of physics-informed QD data structures (``tuning vernacula''); and (iii) extensible libraries of shared measurement protocols enabling an interoperable lab-agnostic measurement stack. By separating algorithm intent from instrument realization, while preserving traceability and supporting typed scripting, FAlCon enables researchers and engineers to exchange, adapt, and deploy characterization and autotuning routines across heterogeneous QD setups. The framework supports all users, ranging from end users running prebuilt algorithms with custom initial conditions to developers extending instrumentation support and contributing new tuning strategies. Although the present release targets QD experiments, other qubit modalities and scientific experiments could reuse FAlCon's modular abstractions by providing new tuning data types and instrument control templates.

2026-03-17T15:20:28Z 19 pages, 3 figures Tyler J. Kovach Daniel Schug Zach D. Merino Mark Friesen Mark A. Eriksson Justyna P. Zwolak http://arxiv.org/abs/2603.16437v1 2026-03-17T12:19:07Z

We present a compilation framework in which dimensional type annotations persist through multi-stage MLIR lowering, enabling the compiler to jointly resolve numeric representation selection and deterministic memory management as coeffect properties of a single program semantic graph (PSG). Dimensional inference determines value ranges; value ranges determine representation selection; representation selection determines word width and memory footprint; and memory footprint, combined with escape classification, determines allocation strategy and cross-target transfer fidelity. The Dimensional Type System (DTS) extends Hindley-Milner unification with constraints drawn from finitely generated abelian groups, yielding inference that is decidable in polynomial time, complete, and principal. Where conventional systems erase dimensional annotations before code generation, DTS carries them as compilation metadata through each lowering stage, making them available where representation and memory placement decisions occur. Deterministic Memory Management (DMM), formalized as a coeffect discipline within the same graph, unifies escape analysis and memory placement with the dimensional framework. Escape analysis classifies value lifetimes into four categories (stack-scoped, closure-captured, return-escaping, byref-escaping), each mapping to a verified allocation strategy. We identify implications for auto-differentiation: the dimensional algebra is closed under the chain rule, and forward-mode gradient computation exhibits a coeffect signature that the framework can verify. The practical consequence is a development environment where escape diagnostics, allocation strategy, representation fidelity, and cache locality estimation are design-time views over the compilation graph.

2026-03-17T12:19:07Z 29 pages, 1 table, 3 appendices with extended examples Houston Haynes http://arxiv.org/abs/2308.09481v5 2026-03-17T11:58:04Z

The languages of mathematical physics and modelling are endowed with a rich ``grammar of dimensions'' that common abstractions of programming languages fail to represent. We propose a dependently typed domain-specific language (embedded in Idris) that captures this grammar. We apply it to formalize basic notions of dimensional analysis: those of dimension function, physical quantity, homomorphic measurement, the covariance principle and Buckingham's Pi theorem. We hope that the language makes mathematical physics more accessible to computer scientists and functional programming more palatable to modellers and physicists.

2023-08-16T14:33:18Z Nicola Botta Patrik Jansson http://arxiv.org/abs/2603.13671v2 2026-03-17T10:06:06Z

Global cryptocurrencies are unbacked and have high transaction cost incurred by global consensus. In contrast, grassroots cryptocurrencies are backed by the goods and services of their issuers -- any person, natural or legal -- and have no transaction cost beyond operating a smartphone. Liquidity in grassroots cryptocurrencies arises from mutual credit via coin exchange among issuers. However, as grassroots coins are redeemable 1-for-1 against any other grassroots coin, the credit-forming exchange must also be 1-for-1, lest prompt redemption after exchange would leave the parties with undue profit or loss. Thus, grassroots coins are incongruent with liquidity through interest-bearing credit. Here we introduce grassroots bonds, which extend grassroots coins with a maturity date, reframing grassroots coins -- cash -- as mature grassroots bonds. Bond redemption generalises coin redemption, allowing the lending of liquid coins in exchange for interest-bearing future-maturity bonds. We show that digital social contracts -- voluntary agreements among persons, specified, fulfilled, and enforced digitally -- can express the full gamut of financial instruments as the voluntary swap of grassroots bonds, including credit lines, loans, sale of debt, forward contracts, options, and escrow-based instruments, and that classical liquidity ratios are applicable just as well to grassroots bonds. Grassroots bonds may thus allow local digital economies to form and grow without initial capital or external credit, harnessing mutual trust within communities into liquidity. The formal specification presented here was used by AI to derive a working implementation of grassroots bonds in GLP, a concurrent logic programming language implemented in Dart for smartphone deployment. The implementation is illustrated by a running multiagent village market scenario, also implemented in GLP by AI.

2026-03-14T00:44:25Z Ehud Shapiro http://arxiv.org/abs/2603.13334v2 2026-03-17T04:15:22Z

Sensitivity-based robustness certification has emerged as a practical approach for certifying neural network robustness, including in settings that require verifiable guarantees. A key advantage of these methods is that certification is performed by concrete numerical computation (rather than symbolic reasoning) and scales efficiently with network size. However, as with the vast majority of prior work on robustness certification and verification, the soundness of these methods is typically proved with respect to a semantic model that assumes exact real arithmetic. In reality deployed neural network implementations execute using floating-point arithmetic. This mismatch creates a semantic gap between certified robustness properties and the behaviour of the executed system. As motivating evidence, we exhibit concrete counterexamples showing that real arithmetic robustness guarantees can fail under floating-point execution, even for previously verified certifiers, with discrepancies becoming pronounced at lower-precision formats such as float16. We then develop a formal, compositional theory relating real arithmetic Lipschitz-based sensitivity bounds to the sensitivity of floating-point execution under standard rounding-error models, specialised to feed-forward neural networks with ReLU activations. We derive sound conditions for robustness under floating-point execution, including bounds on certificate degradation and sufficient conditions for the absence of overflow. We formalize the theory and its main soundness results, and implement an executable certifier based on these principles, which we empirically evaluate to demonstrate its practicality.

2026-03-06T06:13:24Z Toby Murray http://arxiv.org/abs/2505.23135v3 2026-03-16T23:40:56Z

Large language models (LLMs) are increasingly integrated in software development, but ensuring correctness in LLM-generated code remains challenging and often requires costly manual review. Verifiable code generation -- jointly generating code, specifications, and proofs of code-specification alignment -- offers a promising path to address this limitation and further unleash LLMs' benefits in coding. Yet, there exists a significant gap in evaluation: current benchmarks often focus on only individual components rather than providing a holistic evaluation framework of all tasks. In this paper, we introduce VERINA (Verifiable Code Generation Arena), a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions. VERINA consists of 189 manually curated coding tasks in Lean, with detailed problem descriptions, reference implementations, formal specifications, and extensive test suites. Our extensive evaluation of state-of-the-art LLMs reveals significant challenges in verifiable code generation, especially in proof generation, underscoring the need for improving LLM-based theorem provers in verification domains. The best model, OpenAI o3, achieves a 72.6\% code correctness rate, 52.3\% for specification soundness and completeness, and a mere 4.9\% proof success rate (based on one trial per task). We hope VERINA will catalyze progress in verifiable code generation by providing a rigorous and comprehensive benchmark. We release our dataset on https://huggingface.co/datasets/sunblaze-ucb/verina and our evaluation code on https://github.com/sunblaze-ucb/verina.

2025-05-29T06:12:52Z Zhe Ye Zhengxu Yan Jingxuan He Timothe Kasriel Kaiyu Yang Dawn Song http://arxiv.org/abs/2602.23520v3 2026-03-16T23:08:03Z

We construct a structural theory of failure for multi-location encodings. Admissible partial views induce a confusability graph on latent tuples; in the exact coordinate-view model, this graph class is exactly characterized by upward-closed families of coordinate-agreement sets, and exact recovery with a $T$-ary tag is equivalent to $T$-colorability. Repeated composition yields strong powers, so the normalized block-rate sequence converges to asymptotic Shannon capacity bounded above by Lovász-$\vartheta$. The upper theory is sharp whenever confusability is transitive; meet-witnessing and fiber coherence provide checkable sufficient conditions for that collapse. Under an affine restriction, the coordinate structure yields a representable matroid whose rank bounds confusability. The theory applies uniformly to programming-language runtimes, databases, and dependency managers: causal propagation together with provenance observability are necessary and sufficient for verifiable structural integrity.

2026-02-26T21:47:11Z 22 pages. Lean 4 artifact: 25743 lines, 1231 theorems/lemmas across 84 files (0 sorry placeholders) available at https://doi.org/10.5281/zenodo.18141365 Tristan Simas http://arxiv.org/abs/2601.14252v4 2026-03-16T23:06:17Z

Symbolic systems operate over exact identities: variables denote specific objects, pointers target precise memory locations, and database keys refer to singular records. Neural embeddings generalize by compressing away semantic detail, but this compression creates collision ambiguity: multiple distinct entities can share the same representation value. We characterize exactly how much additional information must be supplied to recover precise identity from such representations. The answer is controlled by a single combinatorial object: the collision-fiber geometry of the representation map $π$. Let $A_π=\max_u |π^{-1}(u)|$ be the largest collision fiber. We prove a tight fixed-length converse $L \ge \log_2 A_π$, an exact finite-block scaling law, a pointwise adaptive budget $\lceil \log_2 |π^{-1}(u)|\rceil$, and the rate-distortion tradeoff with an explicit distortion floor when identity bits are withheld. The same fiber geometry determines query complexity and canonical structure for distinguishing families. Because this residual ambiguity is structural rather than representation-specific, symbolic identity mechanisms (handles, keys, pointers, nominal tags) are the necessary system-level complement to any non-injective semantic representation. All main results are machine-checked in Lean 4. Keywords: semantics-aware compression, zero-error coding, neurosymbolic systems, learned representations, side information

2026-01-20T18:58:51Z 16 pages. Lean 4 artifact: 13838 lines, 677 theorems/lemmas across 53 files (0 sorry placeholders) available at https://doi.org/10.5281/zenodo.18123531 Tristan Simas http://arxiv.org/abs/2603.15855v1 2026-03-16T19:38:07Z

The dominant programming languages support nothing but linear text to express domain-specific geometric ideas. What is needed are hybrid languages that allow developers to create visual syntactic constructs so that they can express their ideas with a mix of textual and visual syntax tailored to an application domain. This mix must put the two kinds of syntax on equal footing and, just as importantly, the extended language must not disrupt a programmer's typical workflow. This means that any new visual syntax should be a proper language extension that is composable with other language features. Furthermore, the extensions should also preserve static reasoning about the program. This paper presents Hybrid ClojureScript the first such hybrid programming language. Hybrid ClojureScript allows programmers to add visual interactive syntax and to embed instances of this syntax within a program's text. An enhanced hybrid IDE can then display these embedded instances as mini-GUIs that programmers interact with, while other IDEs will show a textual representation of the syntax. The paper argues the necessity of such an extensibility mechanism, demonstrates the adoptability of the design, and discusses what might be needed to use the design in other languages.

2026-03-16T19:38:07Z to be published in JFP Leif Andersen Michael Ballantyne Cameron Moy Matthias Felleisen Stephen Chang http://arxiv.org/abs/2512.14805v2 2026-03-16T18:57:56Z

The rise of large language models (LLMs) has introduced a new type of programming: natural language programming. Users write prompts, which are instructions in natural language, to direct LLMs to perform tasks such as natural language processing, code generation, reasoning, etc. An emerging area of research enables interoperability between prompts and programs. We present a novel programming abstraction, shared program state, that removes the manual work required to enable interoperability between prompts and program states. With shared program state, programmers can write prompts that directly access program variables, compute with program objects, and implement control flow in the program. We present a schema for specifying natural function interfaces that extend programming systems to support programs with prompts and leverage this schema to specify shared program state as a natural function interface. We implement shared program state in the Nightjar programming system. Nightjar enables programmers to write Python programs containing prompts that share the Python program state. We show that Nightjar programs achieve comparable or higher task accuracy than manually written implementations (+4-19%), while decreasing the lines of code by 39.6% on average. The tradeoff is that Nightjar may incur runtime overhead (0.4-4.3x manual implementations).

2025-12-16T18:41:50Z ICLR 2026 Ellie Y. Cheng Logan Weber Tian Jin Michael Carbin http://arxiv.org/abs/2505.14744v2 2026-03-16T13:59:17Z

Traditionally, in Programming-by-example (PBE) the goal is to synthesize a program from a small set of input-output examples. Lately, PBE has gained traction as a few-shot reasoning benchmark, relaxing the requirement to produce a program artifact altogether which allows transductive methods to directly the missing output sample. Transduction and induction are complementary reasoning modes--where induction derives general rules from examples, transduction leverages the examples directly to infer specific outputs without intermediate generalization. Yet existing approaches either treat them as mutually exclusive or couple them in hybrid structures where one paradigm dictates a fixed trajectory for the other -- undermining the latter's reasoning potential and creating cascading errors. We move away from these hierarchical models and introduce cooperative transductive-inductive problem solving: by interleaving both reasoning modes and ensuring neither unconditionally dominates the other, we preserve the search autonomy and reasoning capacity of each paradigm. We instantiate this concept in TIIPS. Across three PBE domains, TIIPS consistently outperforms state-of-the-art baselines and generates programs that more closely mirror ground-truth trajectories in both syntax and semantics, indicating a better match to the intended program behavior. Our findings highlight cooperative reasoning as a promising new direction for harnessing the full power of symbolic, inductive and neural, transductive reasoning.

2025-05-20T08:23:46Z Janis Zenkner Tobias Sesterhenn Christian Bartelt http://arxiv.org/abs/2507.13792v3 2026-03-16T12:58:02Z

We extend the semantics and type system of a lambda calculus equipped with common constructs to be "resource-aware". That is, the semantics keeps track of the usage of resources, and is stuck, besides in case of type errors, if either a needed resource is exhausted, or a provided resource would be wasted. In such way, the type system guarantees, besides standard soundness, that for well-typed programs there is a computation where no resource gets either exhausted or wasted. The extension is parametric on an arbitrary "grade algebra", modeling an assortment of possible usages, and does not require ad-hoc changes to the underlying language. To this end, the semantics needs to be formalized in big-step style; as a consequence, expressing and proving (resource-aware) soundness is challenging, and is achieved by applying recent techniques based on coinductive reasoning.

2025-07-18T10:06:08Z Preprint submitted to JFP (Journal of Functional Programming) Riccardo Bianchini Francesco Dagnino Paola Giannini Elena Zucca http://arxiv.org/abs/2603.15096v1 2026-03-16T10:49:30Z

In computer science, students are encouraged to learn various programming languages such as Python, C++, and Java, equipping them with a broad range of technical skills and problem-solving capabilities. Nevertheless, the design of objective examination questions to assess students' creativity, problem-solving abilities, and domain knowledge remains a significant challenge. This paper proposes a methodology to address these challenges by leveraging prompt engineering techniques with ChatGPT. Prompt engineering is an efficient technique that optimizes the performance of language models, enabling the automatic generation of high-quality exam questions with varying types and difficulty levels, all without requiring additional fine-tuning of the model. This study applies diverse patterns and templates to generate exam questions that incorporate both theoretical and practical components, thereby facilitating a comprehensive evaluation of students' theoretical understanding and hands-on programming proficiency. A survey was conducted to validate the proposed method, and although certain areas indicated room for improvement, the overall results confirmed its significance and relevance. The generated questions and model answers exhibit quality comparable to, or even surpassing, manually crafted questions while significantly reducing the time and effort required for question preparation. This research demonstrates that automated exam question generation through prompt engineering enhances the quality and efficiency of assessment tools in education, establishing it as a valuable asset for future educational environments.

2026-03-16T10:49:30Z Jongwook Si Sungyoung Kim http://arxiv.org/abs/2602.16291v7 2026-03-16T07:35:47Z

Just as the $λ$-calculus uses three primitives (abstraction, application, variable) as the foundation of functional programming, inheritance-calculus uses three primitives (record, definition, inheritance) as the foundation of declarative programming. By unifying modules, classes, objects, methods, fields, and locals under a single record abstraction, the calculus models inheritance simply as set union. Consequently, composition is inherently commutative, idempotent, and associative, structurally eliminating the multiple-inheritance linearization problem. Its semantics is first-order~\cite{vanemden1976-predicate-logic-semantics, reynolds1972-definitional-interpreters, aczel1977-inductive-definitions}, denotational, and computable by tabling~\cite{tamaki1986-tabled-resolution}, even for cyclic inheritance hierarchies. These three properties extend to the $λ$-calculus, since Böhm tree equivalence~\cite{barendregt1984-lambda-calculus} is fully abstract for the first-iteration approximation of a sublanguage of inheritance-calculus. As a corollary, this establishes a convergence hierarchy $\text{eager} \subsetneq \text{lazy} \subsetneq \text{fixpoint}$ among $λ$-calculi sharing the same $λ$-syntax. Inheritance-calculus is distilled from MIXINv2, a practical implementation in which the same code acts as different function colors~\cite{nystrom2015-function-color}; ordinary arithmetic yields the relational semantics of logic programming~\cite{vanemden1976-predicate-logic-semantics}; $\mathtt{this}$ resolves to multiple targets; and programs are immune to nonextensibility in the sense of the Expression Problem~\cite{wadler1998-expression-problem}. This makes inheritance-calculus strictly more expressive than the $λ$-calculus in both common sense and Felleisen's sense~\cite{felleisen1991-expressive-power}.

2026-02-18T09:17:20Z Bo Yang