https://arxiv.org/api/AV6IWD5HBtsqhC5jWltw3yt5RCU 2026-06-26T07:30:25Z 9951 1200 15 http://arxiv.org/abs/2509.13489v1 2025-09-16T19:41:58Z

A key part of any dependent type-checker is the method for checking whether two types are equal. A common claim is that syntax-directed equality is more performant, although type-directed equality is more expressive. However, this claim is difficult to make precise, since implementations choose only one or the other approach, making a direct comparison impossible. We present some work-in-progress developing a realistic platform for direct, apples-to-apples, comparison of the two approaches, quantifying how much slower type-directed equality checking is, and analyzing why and how it can be improved.

2025-09-16T19:41:58Z Submitted to TyDe 2025 Chester J. F. Gould William J. Bowman http://arxiv.org/abs/2509.16239v1 2025-09-16T17:41:16Z

We introduce the Gödel Mirror, a formal system defined in Lean 4 that treats contradiction as a control signal for recursive structural evolution. Inspired by Gödelian self-reference, our system's operational semantics encode symbolic paradoxes as deterministic transitions. Unlike systems designed to guarantee normalization, the Gödel Mirror is a minimal and verifiable architecture that leverages a controlled, non-terminating loop as a productive feature. Our Lean 4 mechanization proves that self-referential paradoxes are deterministically encapsulated and resolved into new structures without leading to logical explosion, yielding a paraconsistent inference loop: Paradox -> Encapsulate -> Reenter -> Node We argue that this calculus opens a new class of symbolic systems in which contradiction is metabolized into structure, providing a formal basis for agents capable of resolving internal inconsistencies.

2025-09-16T17:41:16Z 10 pages. Preprint submitted to Logical Methods in Computer Science (LMCS) Jhet Chan http://arxiv.org/abs/2509.13261v1 2025-09-16T17:15:28Z

We introduce the Rebound library that supports well-scoped term representations in Haskell and automates the definition of substitution, alpha-equivalence, and other operations that work with binding structures. The key idea of our design is the use of first-class environments that map variables to expressions in some new scope. By statically tracking scopes, users of this library gain confidence that they have correctly maintained the subtle invariants that stem from using de Bruijn indices. Behind the scenes, Rebound uses environments to optimize the application of substitutions, while providing explicit access to these data structures when desired. We demonstrate that this library is expressive by using it to implement a wide range of language features with sophisticated uses of binding and several different operations that use this abstract syntax. Our examples include pi-forall, a tutorial implementation of a type checker for a dependently-typed programming language. Finally, we benchmark Rebound to understand its performance characteristics and find that it produces faster code than competing libraries.

2025-09-16T17:15:28Z 15 pages, 5 figures, 3 tables. To be published in Proceedings of the 18th ACM SIGPLAN International Haskell Symposium (Haskell 2025) Noé De Santo Stephanie Weirich 10.1145/3759164.3759348 http://arxiv.org/abs/2509.13121v1 2025-09-16T14:29:30Z

Fixed point theory studies conditions under which nonexpansive maps on Banach spaces have fixed points. This paper examines the open question of whether every reflexive Banach space has the fixed point property. After surveying classical results, we propose a quantitative framework based on diametral l1 pressure and weighted selection functionals, which measure how much an orbit hull of a fixed point free nonexpansive map can collapse. We prove that if either invariant is uniformly positive, then the space must contain a copy of l1 and thus cannot be reflexive. We present finite dimensional certificates, positive and negative examples, and an x86-64 routine that computes mutual coherence and a lower bound for the pressure. The paper clarifies why existing approaches fail and outlines open problems and ethical considerations.

2025-09-16T14:29:30Z 35 pages, 1 fig., asm Faruk Alpay Hamdi Alakkad http://arxiv.org/abs/2509.13026v1 2025-09-16T12:46:53Z

Strong functors and monads are ubiquitous in Computer Science. More recently, comonads have demonstrated their use in structuring context-dependent notions of computation. However, the dualisation of ``being strong'' property passed somehow unobserved so far. We argue that ``being costrong'' gives a different understanding of how functors can interact with monoidal structures. This work in progress aims to explore costrong functors and their natural properties, with an eye towards the semantics of computations.

2025-09-16T12:46:53Z In Proceedings FROM 2025, arXiv:2509.11877 EPTCS 427, 2025, pp. 141-154 Adriana Balan Department of Mathematical Methods and Models, and Fundamental Sciences Applied in Engineering Research Center, National University of Science and Technology POLITEHNICA Bucharest Silviu-George Pantelimon Department of Computer Science, National University of Science and Technology POLITEHNICA Bucharest 10.4204/EPTCS.427.10 http://arxiv.org/abs/2509.13022v1 2025-09-16T12:45:57Z

Python's typing system has evolved pragmatically into a powerful but theoretically fragmented system, with scattered specifications. This paper proposes a formalization to address this fragmentation. The central contribution is a formal foundation that uses concepts from type theory to demonstrate that Python's type system can be elegantly described. This work aims to serve as a crucial first step toward the future development of type inference tools.

2025-09-16T12:45:57Z In Proceedings FROM 2025, arXiv:2509.11877 EPTCS 427, 2025, pp. 79-97 Andrei Nacu Faculty of Computer Science, Alexandru Ioan Cuza University, Iaşi Dorel Lucanu Faculty of Computer Science, Alexandru Ioan Cuza University, Iaşi 10.4204/EPTCS.427.6 http://arxiv.org/abs/2509.13019v1 2025-09-16T12:45:28Z

Even with the increase of popularity of functional programming, imperative programming remains a key programming paradigm, especially for programs operating at lower levels of abstraction. When such software offers key components of a Trusted Computing Base (TCB), e.g. an operating system kernel, it becomes desirable to provide mathematical correctness proofs. However, current real-world imperative programming languages possess "expressive", i.e. overly permissive, semantics. Thus, producing correctness proofs of such programs becomes tedious and error-prone, requiring to take care of numerous "administrative" details. Ideally, a proof-oriented imperative language should feature well-behaved semantics while allowing imperative idioms. To obtain a high-degree of confidence in the correctness of such a language, its tools should be developed inside a proof-assistant such that program proofs are machine checked. We present GallinaC, a shallow embedding of a Turing-complete imperative language directly inside the functional programming language of the Rocq proof assistant, Gallina. In particular, it features a truly generic and unbounded while loop. Having a functional core means proofs about GallinaC programs may use the same tactics as proofs about pure functional ones. Work on GallinaC is still under progress, but we present first promising results. A prototype implementation has shown the viability of GallinaC with the correctness proof of a list reversal procedure for linked-lists of unknown size. We currently focus on the forward simulation between the GallinaC intermediate representation (IR) and Cminor, the entry language of the CompCert back-end.

2025-09-16T12:45:28Z In Proceedings FROM 2025, arXiv:2509.11877 EPTCS 427, 2025, pp. 24-32 Frédéric Fort David Nowak Vlad Rusu 10.4204/EPTCS.427.2 http://arxiv.org/abs/2509.13006v1 2025-09-16T12:18:41Z

Linear Programming (LP) is widely applied in industry and is a key component of various other mathematical problem-solving techniques. Recent work introduced an LP compiler translating polynomial-time, polynomial-space algorithms into polynomial-size LPs using intuitive high-level programming languages, offering a promising alternative to manually specifying each set of constraints through Algebraic Modeling Languages (AMLs). However, the resulting LPs, while polynomial in size, are often extremely large, posing challenges for existing LP solvers. In this paper, we propose a novel approach for generating substantially smaller LPs from algorithms. Our goal is to establish minimum-size compact LP formulations for problems in P having natural formulations with exponential extension complexities. Our broader vision is to enable the systematic generation of Compact Integer Programming (CIP) formulations for problems with exponential-size IPs having polynomial-time separation oracles. To this end, we introduce a hierarchical linear pipelining technique that decomposes nested program structures into synchronized regions with well-defined execution transitions -- functions of compile-time parameters. This decomposition allows us to localize LP constraints and variables within each region, significantly reducing LP size without the loss of generality, ensuring the resulting LP remains valid for all inputs of size $n$. We demonstrate the effectiveness of our method on two benchmark problems -- the makespan problem, which has exponential extension complexity, and the weighted minimum spanning tree problem -- both of which have exponential-size natural LPs. Our results show up to a $25$-fold reduction in LP size and substantial improvements in solver performance across both commercial and non-commercial LP solvers.

2025-09-16T12:18:41Z Preliminary version will appear in CASCON 2025 Shermin Khosravi David Bremner http://arxiv.org/abs/2412.10483v3 2025-09-16T02:52:43Z

Automated program verification has always been an important component of building trustworthy software. While the analysis of real-world programs remains a theoretical challenge, the automation of loop invariant analysis has effectively resolved the problem. However, real-world programs that often mix complex data structures and control flows pose challenges to traditional loop invariant generation tools. To enhance the applicability of invariant generation techniques, we proposed ACInv, an Automated Complex program loop Invariant generation tool, which combines static analysis with Large Language Models (LLMs) to generate the proper loop invariants. We utilize static analysis to extract the necessary information for each loop and embed it into prompts for the LLM to generate invariants for each loop. Subsequently, we employ an LLM-based evaluator to assess the generated invariants, refining them by either strengthening, weakening, or rejecting them based on their correctness, ultimately obtaining enhanced invariants. We conducted experiments on ACInv, which showed that ACInv outperformed previous tools on data sets with data structures, and maintained similar performance to the state-of-the-art tool AutoSpec on numerical programs without data structures. For the total data set, ACInv can solve 21% more examples than AutoSpec and can generate reference data structure templates.

2024-12-13T10:36:18Z 26 pages, 11 figures Ruibang Liu Minyu Chen Ling-I Wu Jingyu Ke Guoqiang Li http://arxiv.org/abs/2509.12593v1 2025-09-16T02:39:57Z

In the domain of Programmable Logic Controller (PLC) programming, converting a Ladder Diagram (LD) into a Sequential Function Chart (SFC) is an inherently challenging problem, primarily due to the lack of domain-specific knowledge and the issue of state explosion in existing algorithms. However, the rapid development of Artificial Intelligence (AI) - especially Large Language Model (LLM) - offers a promising new approach. Despite this potential, data-driven approaches in this field have been hindered by a lack of suitable datasets. To address this gap, we constructed several datasets consisting of paired textual representations of SFC and LD programs that conform to the IEC 61131-3 standard. Based on these datasets, we explored the feasibility of automating the LD-SFC conversion using LLM. Our preliminary experiments show that a fine-tuned LLM model achieves up to 91% accuracy on certain dataset, with the lowest observed accuracy being 79%, suggesting that with proper training and representation, LLMs can effectively support LD-SFC conversion. These early results highlight the viability and future potential of this approach.

2025-09-16T02:39:57Z Yimin Zhang Mario de Sousa 10.1109/ETFA65518.2025.11205542 http://arxiv.org/abs/2405.08965v6 2025-09-15T18:21:33Z

Software development is shifting from traditional programming to AI-integrated applications that leverage generative AI and large language models (LLMs) during runtime. However, integrating LLMs remains complex, requiring developers to manually craft prompts and process outputs. Existing tools attempt to assist with prompt engineering, but often introduce additional complexity. This paper presents Meaning-Typed Programming (MTP), a novel paradigm that abstracts LLM integration through intuitive language-level constructs. By leveraging the inherent semantic richness of code, MTP automates prompt generation and response handling without additional developer effort. We introduce the (1) by operator for seamless LLM invocation, (2) MT-IR, a meaning-based intermediate representation for semantic extraction, and (3) MT-Runtime, an automated system for managing LLM interactions. We implement MTP in Jac, a programming language that supersets Python, and find that MTP significantly reduces coding complexity while maintaining accuracy and efficiency. MTP significantly reduces development complexity, lines of code modifications needed, and costs while improving run-time performance and maintaining or exceeding the accuracy of existing approaches. Our user study shows that developers using MTP completed tasks 3.2x faster with 45% fewer lines of code compared to existing frameworks. Moreover, MTP demonstrates resilience even when up to 50% of naming conventions are degraded, demonstrating robustness to suboptimal code. MTP is developed as part of the Jaseci open-source project, and is available under the module byLLM.

2024-05-14T21:12:01Z OOPSLA 2025 Jayanaka L. Dantanarayana Yiping Kang Kugesan Sivasothynathan Christopher Clarke Baichuan Li Savini Kashmira Krisztian Flautner Lingjia Tang Jason Mars http://arxiv.org/abs/2509.11901v1 2025-09-15T13:24:41Z

Control operators, such as exceptions and effect handlers, provide a means of representing computational effects in programs abstractly and modularly. While most theoretical studies have focused on multi-shot control operators, one-shot control operators -- which restrict the use of captured continuations to at most once -- are gaining attention for their balance between expressiveness and efficiency. This study aims to fill the gap. We present a mathematically rigorous comparison of the expressive power among one-shot control operators, including effect handlers, delimited continuations, and even asymmetric coroutines. Following previous studies on multi-shot control operators, we adopt Felleisen's macro-expressiveness as our measure of expressiveness. We verify the folklore that one-shot effect handlers and one-shot delimited-control operators can be macro-expressed by asymmetric coroutines, but not vice versa. We explain why a previous informal argument fails, and how to revise it to make a valid macro-translation.

2025-09-15T13:24:41Z Full version of the paper accepted at APLAS 2025. Includes appendices with proofs. 59 pages Kentaro Kobayashi Yukiyoshi Kameyama http://arxiv.org/abs/2509.11877v1 2025-09-15T12:57:29Z

This volume contains the proceedings of the 9th Working Formal Methods Symposium, which was held at the Alexandru Ioan Cuza University, Iaşi, Romania on September 17-19, 2025.

2025-09-15T12:57:29Z EPTCS 427, 2025 Andrei Arusoaie Alexandru Ioan Cuza University of Iaşi Horaţiu Cheval University of Bucharest Radu Iosif Verimag, CNRS, University of Grenoble Alpes 10.4204/EPTCS.427 http://arxiv.org/abs/2509.10236v2 2025-09-15T08:39:52Z

We introduce Stencil-Lifting, a novel system for automatically converting stencil kernels written in low-level languages in legacy code into semantically equivalent Domain-Specific Language (DSL) implementations. Targeting the efficiency bottlenecks of existing verified lifting systems, Stencil-Lifting achieves scalable stencil kernel abstraction through two key innovations. First, we propose a hierarchical recursive lifting theory that represents stencil kernels, structured as nested loops, using invariant subgraphs, which are customized data dependency graphs that capture loop-carried computation and structural invariants. Each vertex in the invariant subgraph is associated with a predicate-based summary, encoding its computational semantics. By enforcing self-consistency across these summaries, Stencil-Lifting ensures the derivation of correct loop invariants and postconditions for nested loops, eliminating the need for external verification. Second, we develop a hierarchical recursive lifting algorithm that guarantees termination through a convergent recursive process, avoiding the inefficiencies of search-based synthesis. The algorithm efficiently derives the valid summaries of stencil kernels, and its completeness is formally proven. We evaluate Stencil-Lifting on diverse stencil benchmarks from two different suites and on four real-world applications. Experimental results demonstrate that Stencil-Lifting achieves 31.62$\times$ and 5.8$\times$ speedups compared to the state-of-the-art verified lifting systems STNG and Dexter, respectively, while maintaining full semantic equivalence. Our work significantly enhances the translation efficiency of low-level stencil kernels to DSL implementations, effectively bridging the gap between legacy optimization techniques and modern DSL-based paradigms.

2025-09-12T13:30:18Z 33 pages, 12 figures. Submitted to OOPSLA2'25 Mingyi Li Junmin Xiao Siyan Chen Hui Ma Xi Chen Peihua Bao Liang Yuan Guangming Tan 10.1145/3763159 http://arxiv.org/abs/2509.11559v1 2025-09-15T03:45:53Z

RLWE-based Fully Homomorphic Encryption (FHE) schemes add some small \emph{noise} to the message during encryption. The noise accumulates with each homomorphic operation. When the noise exceeds a critical value, the FHE circuit produces an incorrect output. This makes developing FHE applications quite subtle, as one must closely track the noise to ensure correctness. However, existing libraries and compilers offer limited support to statically track the noise. Additionally, FHE circuits are also plagued by wraparound errors that are common in finite modulus arithmetic. These two limitations of existing compilers and libraries make FHE applications too difficult to develop with confidence. In this work, we present a \emph{correctness-oriented} IR, Intermediate Language for Arithmetic circuits, for type-checking circuits intended for homomorphic evaluation. Our IR is backed by a type system that tracks low-level quantitative bounds (e.g., ciphertext noise) without using the secret key. Using our type system, we identify and prove a strong \emph{functional correctness} criterion for \ila circuits. Additionally, we have designed \ila to be maximally general: our core type system does not directly assume a particular FHE scheme, but instead axiomatizes a \emph{model} of FHE. We instantiate this model with the exact FHE schemes (BGV, BFV and TFHE), and obtain functional correctness for free.

2025-09-15T03:45:53Z Tarakaram Gollamudi Anitha Gollamudi Joshua Gancher