https://arxiv.org/api/hLUh32AYl84QCJ8dJDXlYH4/4/w 2026-06-21T18:17:51Z 9918 780 15 http://arxiv.org/abs/2111.13384v9 2026-01-07T13:15:09Z

Object-oriented programming (OOP) is one of the most popular paradigms used for building software systems. However, despite its industrial and academic popularity, OOP is still missing a formal apparatus similar to \(λ\)-calculus, which functional programming is based on. A number of attempts were made to formalize OOP, but none of them managed to cover all the features available in modern OO programming languages, such as C++ or Java. We have made yet another attempt and created \(\varphi\)-calculus. This paper does not demonstrate the practical use or effect of \\(varphi\) but merely explains it.

2021-11-26T09:42:45Z Yegor Bugayenko Maxim Trunnikov http://arxiv.org/abs/2601.03897v1 2026-01-07T13:06:07Z

We present an approach to implement binary search trees in the rule-based graph programming language GP 2. Our implementation uses GP 2's rooted graph transformation rules to be fast and supports insertion, deletion and query operations. We argue that the worst-case runtime for each of the operations is O(n) for a tree with n nodes. In addition, we expect that, on average, the operations run in time O(log(n)). Hence the implementation would match the time complexity of binary search trees implementations in imperative languages.

2026-01-07T13:06:07Z In Proceedings GCM 2025, arXiv:2601.03249 EPTCS 440, 2026, pp. 6-12 Ziad Ismaili Alaoui Department of Computer Science, University of Liverpool, Liverpool, United Kingdom Detlef Plump Department of Computer Science, University of York, York, United Kingdom 10.4204/EPTCS.440.2 http://arxiv.org/abs/2412.14043v2 2026-01-07T12:32:53Z

Loop invariants are properties of a program loop that hold both before and after each iteration of the loop. They are often used to verify programs and ensure that algorithms consistently produce correct results during execution. Consequently, generating invariants becomes a crucial task for loops. We specifically focus on polynomial loops, where both the loop conditions and the assignments within the loop are expressed as polynomials. Although computing polynomial invariants for general loops is undecidable, efficient algorithms have been developed for certain classes of loops. For instance, when all assignments within a while loop involve linear polynomials, the loop becomes solvable. In this work, we study the more general case, where the polynomials can have arbitrary degrees. Using tools from algebraic geometry, we present two algorithms designed to generate all polynomial invariants within a given vector subspace, for a branching loop with nondeterministic conditional statements. These algorithms combine linear algebraic subroutines with computations on polynomial ideals. They differ depending on whether the initial values of the loop variables are specified or treated as parameters. Additionally, we present a much more efficient algorithm for generating polynomial invariants of a specific form, applicable to all initial values. This algorithm avoids expensive ideal computations.

2024-12-18T16:58:48Z 44 pages, 1 figure Journal of Symbolic Computation Vol. 135, 2026, p.102551 Erdenebayar Bayarmagnai Fatemeh Mohammadi Rémi Prébet 10.1016/j.jsc.2025.102551 http://arxiv.org/abs/2507.11731v2 2026-01-07T12:09:28Z

Picat is a logic-based, multi-paradigm programming language that integrates features from logic, functional, constraint, and imperative programming paradigms. This paper presents solutions to several problems from the 2024 Advent of Code (AoC). While AoC problems are not designed for any specific programming language, certain problem types, such as reverse engineering and path-finding, are particularly well-suited to Picat due to its built-in constraint solving, pattern matching, backtracking, and dynamic programming with tabling. This paper demonstrates that Picat's features, especially its SAT-based constraint solving and tabling, enable concise, declarative, and highly efficient implementations of problems that would require significantly more effort in imperative languages.

2025-07-15T20:58:31Z In Proceedings ICLP 2025, arXiv:2601.00047 EPTCS 439, 2026, pp. 528-541 Neng-Fa Zhou CUNY Brooklyn College and Graduate Center Cristian Grozea Fraunhofer Institute FOKUS Håkan Kjellerstrand Independent Researcher, hakank.org Oisín Mac Fhearaí 10.4204/EPTCS.439.36 http://arxiv.org/abs/2601.03854v1 2026-01-07T12:09:14Z

We present a framework for synthesising formulas in first-order logic (FOL) from examples, which unifies and advances state-of-the-art approaches for inference of transition system invariants. To do so, we study and categorise the existing methodologies, encoding techniques in their formula synthesis via answer set programming (ASP). Based on the derived categorisation, we propose orthogonal slices, a new technique for formula enumeration that partitions the search space into manageable chunks, enabling two approaches for incremental candidate pruning. Using a combination of existing techniques for first-order (FO) invariant synthesis and the orthogonal slices implemented in our framework FORCE, we significantly accelerate a state-of-the-art algorithm for distributed system invariant inference. We also show that our approach facilitates composition of different invariant inference frameworks, allowing for novel optimisations.

2026-01-07T12:09:14Z In Proceedings ICLP 2025, arXiv:2601.00047 EPTCS 439, 2026, pp. 511-527 Ziyi Yang George Pîrlea Ilya Sergey 10.4204/EPTCS.439.35 http://arxiv.org/abs/2601.03849v1 2026-01-07T12:08:30Z

LPTP (Logic Program Theorem Prover) is an interactive natural-deduction-based theorem prover for pure Prolog programs with negation as failure, unification with the occurs check, and a restricted but extensible set of built-in predicates. With LPTP, one can formally prove termination and partial correctness of such Prolog programs. LPTP was designed in the mid-1990's by Robert F. Staerk. It is written in ISO-Prolog and comes with an Emacs user-interface. From a theoretical point of view, in his publications about LPTP, Staerk associates a set of first-order axioms IND(P) to the considered Prolog program P. IND(P) contains the Clark's equality theory for P, definitions of success, failure and termination for each user-defined logic procedure in P, axioms relating these three points of view, and an axiom schema for proving inductive properties. LPTP is thus a dedicated proof editor where these axioms are hard-wired. We propose to translate these axioms as first-order formulas (FOFs), and apply automated theorem provers to check the property of interest. Using FOF as an intermediary language, we experiment the use of automated theorem provers for Prolog program verification. We evaluate the approach over a benchmark of about 400 properties of Prolog programs from the library available with LPTP. Both the compiler which generates a set of FOF files from a given input Prolog program together with its properties and the benchmark are publicly available.

2026-01-07T12:08:30Z In Proceedings ICLP 2025, arXiv:2601.00047 EPTCS 439, 2026, pp. 469-481 Fred Mesnard LIM, université de La Réunion Thierry Marianne LIM, université de La Réunion Étienne Payet LIM, université de La Réunion 10.4204/EPTCS.439.32 http://arxiv.org/abs/2601.03848v1 2026-01-07T12:08:15Z

We present automated theorem provers for the first-order logic of here and there (HT). They are based on a native sequent calculus for the logic of HT and an axiomatic embedding of the logic of HT into intuitionistic logic. The analytic proof search in the sequent calculus is optimized by using free variables and skolemization. The embedding is used in combination with sequent, tableau and connection calculi for intuitionistic first-order logic. All provers are evaluated on a large benchmark set of first-order formulas, providing a foundation for the development of more efficient HT provers.

2026-01-07T12:08:15Z In Proceedings ICLP 2025, arXiv:2601.00047 EPTCS 439, 2026, pp. 453-468 Jens Otten University of Pernambuco Torsten Schaub University of Potsdam 10.4204/EPTCS.439.31 http://arxiv.org/abs/2504.04962v4 2026-01-07T12:02:24Z

Constraint Handling Rules (CHR) is a rule-based programming language which is typically embedded into a general-purpose language. There exists a plethora of implementations for numerous host languages. However, the existing implementations often re-invent the way to embed CHR, which impedes maintenance and weakens assertions of correctness. To formalize and thereby standardize the embedding into arbitrary host languages, we introduced the framework FreeCHR and proved it to be a valid representation of classical ground CHR. Until now, this framework only includes a translation of the very abstract operational semantics which, due to its abstract nature, is not a sufficient base for practical implementations. In this paper we present a translation of the refined operational semantics for FreeCHR and prove it to be both a valid concretization of the very abstract semantics of FreeCHR, and an equivalent representation of the refined semantics of CHR. This will establish implementations of FreeCHR as equivalent in behavior and expressiveness to existing implementations of CHR.

2025-04-07T11:51:07Z In Proceedings ICLP 2025, arXiv:2601.00047 EPTCS 439, 2026, pp. 278-293 Sascha Rechenberger Ulm University Thom Frühwirth Ulm University 10.4204/EPTCS.439.20 http://arxiv.org/abs/2601.03836v1 2026-01-07T12:02:09Z

Logic programming languages present clear advantages in terms of declarativeness and conciseness. However, the ideas of logic programming have been met with resistance in other programming communities, and have not generally been adopted by other paradigms and languages. This paper proposes a novel way to incorporate logic programming in an existing codebase in a typed functional programming language. Our approach integrates with the host language without sacrificing static typing, and leverages strengths of typed functional programming such as polymorphism and higher-order. We do so by combining three ideas. First, we use the extensible types technique to allow values of the host language to contain logic variables. Second, we implement a unification algorithm that works for any data structure that supports certain operations.Third, we introduce a domain-specific language to define and query predicates. We demonstrate our proposal via a series of examples, and provide aids to make the notation convenient for users, showing that the proposed approach is not just technically possible but also practical. Our ideas have been implemented in the language Haskell with very good results.

2026-01-07T12:02:09Z In Proceedings ICLP 2025, arXiv:2601.00047 EPTCS 439, 2026, pp. 248-262 Ivan Perez KBR @ NASA Ames Research Center Angel Herranz Universidad Politecnica de Madrid 10.4204/EPTCS.439.18 http://arxiv.org/abs/2601.03768v1 2026-01-07T10:02:17Z

Proof engineering is notoriously labor-intensive: proofs that are straightforward on paper often require lengthy scripts in theorem provers. Recent advances in large language models (LLMs) create new opportunities for proof automation: modern LLMs not only generate proof scripts, but also support agentic behavior, exploring codebases and iteratively refining their outputs against prover feedback. These advances enable an emerging scheme where LLM-based agents undertake most proof engineering under human guidance. Humans provide mathematical insight (definitions, theorems, proof strategies); agents handle the mechanical work of proof development. We call this scheme agentic proof automation. We present this scheme through a case study: mechanizing the semantic type soundness of a sophisticated formal system, System Capless, in Lean 4, comprising over 14,000 lines of code. Using off-the-shelf LLM agents with a single lightweight proof-checking tool, the agents completed 189 proof engineering tasks with an 87% success rate, only 16% requiring human intervention. The case study demonstrates that agents are capable proof engineers that substantially boost productivity, though they fall short in creative reasoning and still require human guidance in certain cases. We release an interactive explorer where readers can examine all agent interactions; the mechanization is open-sourced for experiments and extensions.

2026-01-07T10:02:17Z Yichen Xu Martin Odersky http://arxiv.org/abs/2601.03249v1 2026-01-06T18:47:06Z

This volume contains the post-proceedings of the Sixteenth International Workshop on Graph Computation Models (GCM 2025). The workshops took place in Koblenz, Germany on June 10 as part of STAF (Software Technologies: Applications and Foundations). Graphs are common mathematical structures that are visual and intuitive. They constitute a natural and seamless way for system modeling in science, engineering, and beyond, including computer science, biology, and business process modeling. Graph computation models constitute a class of very high-level models where graphs are first-class citizens. The aim of the International GCM Workshop series is to bring together researchers interested in all aspects of computation models based on graphs and graph transformation. It promotes the cross-fertilizing exchange of ideas and experiences among senior and young researchers from the different communities interested in the foundations, applications, and implementations of graph computation models and related areas.

2026-01-06T18:47:06Z EPTCS 440, 2026 Leen Lambers Brandenburg University of Technology Cottbus-Senftenberg Oszkár Semeráth Budapest University of Technology and Economics 10.4204/EPTCS.440 http://arxiv.org/abs/2502.03203v6 2026-01-06T14:20:59Z

The Spectre speculative side-channel attacks pose formidable threats for security. Research has shown that code following the cryptographic constant-time discipline can be efficiently protected against Spectre v1 using a selective variant of Speculative Load Hardening (SLH). SLH was, however, not strong enough for protecting non-cryptographic code, leading to the introduction of Ultimate SLH, which provides protection for arbitrary programs, but has too large overhead for general use, since it conservatively assumes that all data is secret. In this paper we introduce a flexible SLH notion that achieves the best of both worlds by generalizing both Selective and Ultimate SLH. We give a suitable security definition for such transformations protecting arbitrary programs: any transformed program running with speculation should not leak more than what the source program leaks sequentially. We formally prove using the Rocq prover that two flexible SLH variants enforce this relative security guarantee. As easy corollaries we also obtain that, in our setting, Ultimate SLH enforces our relative security notion, and two selective SLH variants enforce speculative constant-time security.

2025-02-05T14:23:43Z CSF'25 camera-ready version extended with appendices and a few typos fixed Jonathan Baumann Roberto Blanco Léon Ducruet Sebastian Harwig Catalin Hritcu http://arxiv.org/abs/2601.02218v1 2026-01-05T15:43:09Z

Compilers are essential for the performance and correct execution of software and hold universal relevance across various scientific disciplines. Despite this, there is a notable lack of tools for testing and evaluating them, especially within the adaptable Multi-Level Intermediate Representation (MLIR) context. This paper addresses the need for a tool that can accommodate MLIR's extensibility, a feature not provided by previous methods such as Csmith. Here we introduce MLIR-Smith, a novel random program generator specifically designed to test and evaluate MLIR-based compiler optimizations. We demonstrate the utility of MLIR-Smith by conducting differential testing on MLIR, LLVM, DaCe, and DCIR, which led to the discovery of multiple bugs in these compiler pipelines. The introduction of MLIR-Smith not only fills a void in the realm of compiler testing but also emphasizes the importance of comprehensive testing within these systems. By providing a tool that can generate random MLIR programs, this paper enhances our ability to evaluate and improve compilers and paves the way for future tools, potentially shaping the wider landscape of software testing and quality assurance.

2026-01-05T15:43:09Z Berke Ates Filip Dobrosavljević Theodoros Theodoridis Zhendong Su http://arxiv.org/abs/2601.02060v1 2026-01-05T12:33:37Z

Functional programming provides strong foundations for developing reliable and secure software systems, yet its adoption remains not widespread due to the steep learning curve. Recent advances in Large Language Models (LLMs) for code generation present new opportunities to lower these barriers. However, extensive evaluations of LLMs largely focus on imperative programming languages, and their capabilities in functional programming languages (FP) remain underexplored. To address this gap, we introduce FPEval, a holistic evaluation framework built on FPBench, a new benchmark of 721 programming tasks across three difficulty levels on three mainstream FP languages: Haskell, Ocaml and Scala. FPEval provides compehensive evaluation infrastructures with both test validations with comprehensive test suites and static analysis tools to assess both functional correctness and code style and maintainability. Using this framework, we evaluate state-of-the-art LLMs, including GPT-3.5, GPT-4o, and GPT-5, for code generation in functional programming languages and Java as an imperative baseline. Our results demonstrate that LLM performance in functional programming improves substantially with model advancement; however, error rates remain significantly higher in purely functional languages (Haskell and OCaml) than in hybrid (Scala) or imperative (Java) languages. Moreover, LLMs frequently generate non-idiomatic functional code that follows imperative patterns, raising concerns about code style and long-term maintainability. Finally, we show that LLMs can partially self-repair both correctness and quality issues when provided with static analysis feedback and hand-crafted instructions for common types of issues.

2026-01-05T12:33:37Z Nguyet-Anh H. Lang Eric Lang Thanh Le-Cong Bach Le Quyet-Thang Huynh http://arxiv.org/abs/2601.02045v1 2026-01-05T12:02:57Z

This survey has provided a systematic overview of the emerging field of LLM-enabled compilation by addressing several key research questions. We first answered how LLMs are being integrated by proposing a comprehensive, multi-dimensional taxonomy that categorizes works based on their Design Philosophy (Selector, Translator, Generator), LLM Methodology, their operational Level of Code Abstraction, and the specific Task Type they address. In answering what advancements these approaches offer, we identified three primary benefits: the democratization of compiler development, the discovery of novel optimization strategies, and the broadening of the compiler's traditional scope. Finally, in addressing the field's challenges and opportunities, we highlighted the critical hurdles of ensuring correctness and achieving scalability, while identifying the development of hybrid systems as the most promising path forward. By providing these answers, this survey serves as a foundational roadmap for researchers and practitioners, charting the course for a new generation of LLM-powered, intelligent, adaptive and synergistic compilation tools.

2026-01-05T12:02:57Z Accepted by CCF Transactions on High Performance Computing Shuoming Zhang Jiacheng Zhao Qiuchu Yu Chunwei Xia Zheng Wang Xiaobing Feng Huimin Cui 10.1007/s42514-025-00270-x