https://arxiv.org/api/ZdpykaExM1n0RafYdBqFp/prX9o 2026-06-26T15:57:02Z 9951 1305 15 http://arxiv.org/abs/2508.12572v2 2025-08-20T12:42:22Z

It is well known that the reachability problem for simply-typed lambda calculus with recursive definitions and finite base-type values (finitary PCF) is decidable. A recent paper by Dal Lago and Ghyselen has shown that the same problem becomes undecidable when the language is extended with algebraic effect and handlers (effect handlers). We show that, perhaps surprisingly, the problem becomes decidable even with effect handlers when the type system is extended with answer type modification (ATM). A natural intuition may find the result contradictory, because one would expect allowing ATM makes more programs typable. Indeed, this intuition is correct in that there are programs that are typable with ATM but not without it, as we shall show in the paper. However, a corollary of our decidability result is that the converse is true as well: there are programs that are typable without ATM but becomes untypable with ATM, and we will show concrete examples of such programs in the paper. Our decidability result is proven by a novel continuation passing style (CPS) transformation that transforms an ATM-typable finitary PCF program with effect handlers to a finitary PCF program without effect handlers. Additionally, as another application of our CPS transformation, we show that every recursive-function-free ATM-typable finitary PCF program with effect handlers terminates, while there are (necessarily ATM-untypable) recursive-function-free finitary PCF programs with effect handlers that may diverge. Finally, we disprove a claim made in a recent work that proved a similar but strictly weaker decidability result. We foresee our decidability result to lay a foundation for developing verification methods for programs with effect handlers, just as the decidability result for reachability of finitary PCF has done such for programs without effect handlers.

2025-08-18T02:14:59Z Full version of the paper to appear in APLAS 2025 Ryunosuke Endo Tachio Terauchi http://arxiv.org/abs/2508.14614v1 2025-08-20T11:01:16Z

Component-based synthesis (CBS) aims to generate loop-free programs from a set of libraries whose methods are annotated with specifications and whose output must satisfy a set of logical constraints, expressed as a query. The effectiveness of a CBS algorithm critically depends on the severity of the constraints imposed by the query. The more exact these constraints are, the sparser the space of feasible solutions. This maxim also applies when we enrich the expressiveness of the specifications affixed to library methods. In both cases, the search must now contend with constraints that may only hold over a small number of the possible execution paths that can be enumerated by a CBS procedure. In this paper, we address this challenge by equipping CBS search with the ability to reason about logical similarities among the paths it explores. Our setting considers library methods equipped with refinement-type specifications that enrich ordinary base types with a set of rich logical qualifiers to constrain the set of values accepted by that type. We perform a search over a tree automata variant called Qualified Tree Automata that intelligently records information about enumerated terms, leveraging subtyping constraints over the refinement types associated with these terms to enable reasoning about similarity among candidate solutions as search proceeds, thereby avoiding exploration of semantically similar paths. We present an implementation of this idea in a tool called \name, and provide a comprehensive evaluation that demonstrates \name's ability to synthesize solutions to complex CBS queries that go well-beyond the capabilities of the existing state-of-the-art.

2025-08-20T11:01:16Z Ashish Mishra Suresh Jagannathan http://arxiv.org/abs/2508.13948v1 2025-08-19T15:37:29Z

Large Language Models (LLMs) require sophisticated prompting, yet current practices face challenges in structure, data integration, format sensitivity, and tooling. Existing methods lack comprehensive solutions for organizing complex prompts involving diverse data types (documents, tables, images) or managing presentation variations systematically. To address these gaps, we introduce POML (Prompt Orchestration Markup Language). POML employs component-based markup for logical structure (roles, tasks, examples), specialized tags for seamless data integration, and a CSS-like styling system to decouple content from presentation, reducing formatting sensitivity. It includes templating for dynamic prompts and a comprehensive developer toolkit (IDE support, SDKs) to improve version control and collaboration. We validate POML through two case studies demonstrating its impact on complex application integration (PomLink) and accuracy performance (TableQA), as well as a user study assessing its effectiveness in real-world development scenarios.

2025-08-19T15:37:29Z All findings in this paper are derived from a POML snapshot as of February 2025 Yuge Zhang Nan Chen Jiahang Xu Yuqing Yang http://arxiv.org/abs/2508.13611v1 2025-08-19T08:16:42Z

Departing from Larsen's concept of parameterized bisimilarity of processes with respect to interaction with environments, we start an exploration of its natural weakening: bisimilarity of unrestricted join interactions with environments. Parameterized bisimilarity relates processes p and q with respect to an environment e if p and q behave bi-similarly while joining -- respectively the same -- transitions from e. The weakened variant relates processes p and q with respect to environment e if the join-interaction processes p & e and q & e of p and q with e are bisimilar. (Hereby join interactions r & f facilitate a step with label a to r' & f' if and only if r and f permit a-steps to r' and f' , respectively.) Join-interaction parameterized (ji-parameterized) bisimilarity coincides with parameterized bisimilarity for deterministic environments, but that it is a coarser equivalence in general. We explain how Larsen's concept can be recovered from ji-parameterized bisimilarity by 'determinizing' interactions. We show that by adaptation to simulatability (simulation preorder) the same concept arises: parameterized simulatability coincides with ji-parameterized simulatability. For the discrimination preorder of (ji-)parameterized simulatability on environments we obtain the same result as Larsen did for parameterized bisimilarity. Also, we give a modal-logic characterization of (ji-)parameterized simulatability. Finally we gather open problems, and provide an outlook on our current related work.

2025-08-19T08:16:42Z In Proceedings ICE 2025, arXiv:2508.12308 EPTCS 425, 2025, pp. 36-54 Clemens Grabmayer Maurizio Murgia 10.4204/EPTCS.425.4 http://arxiv.org/abs/2508.13610v1 2025-08-19T08:16:28Z

User Interface Description Languages (UIDLs) are high-level languages that facilitate the development of Human-Machine Interfaces, such as Graphical User Interface (GUI) applications. They usually provide first-class primitives to specify how the program reacts to an external event (user input, network message), and how data flows through the program. Although these domain-specific languages are now widely used to implement safety-critical GUIs, little work has been invested in their formalization and verification. In this paper, we propose a denotational semantic model for a core reactive UIDL, Smalite, which we argue is expressive enough to encode constructs from more realistic languages. This preliminary work may be used as a stepping stone to produce a formally verified compiler for UIDLs.

2025-08-19T08:16:28Z In Proceedings ICE 2025, arXiv:2508.12308 EPTCS 425, 2025, pp. 21-35 Basile Pesin Federation ENAC ISAE-SUPAERO ONERA, Universite de Toulouse, France Celia Picard Federation ENAC ISAE-SUPAERO ONERA, Universite de Toulouse, France Cyril Allignol Federation ENAC ISAE-SUPAERO ONERA, Universite de Toulouse, France 10.4204/EPTCS.425.3 http://arxiv.org/abs/2508.18231v1 2025-08-18T18:10:27Z

Object-centric process mining investigates the intertwined behavior of multiple objects in business processes. From object-centric event logs, object-centric Petri nets (OCPN) can be discovered to replay the behavior of processes accessing different object types. Although they indicate how objects flow through the process and co-occur in events, OCPNs remain underspecified about the relationships of objects. Hence, they are not able to represent synchronization, i.e. executing objects only according to their intended relationships, and fail to identify violating executions. Existing formal modeling approaches, such as object-centric Petri nets with identifiers (OPID), represent object identities and relationships to synchronize them correctly. However, OPID discovery has not yet been studied. This paper uses explicit data models to bridge the gap between OCPNs and formal OPIDs. We identify the implicit assumptions of stable many-to-one relationships in object-centric event logs, which implies synchronization of related objects. To formally underpin this observation, we combine OCPNs with explicit stable many-to-one relationships in a rigorous mapping from OCPNs to OPIDs explicitly capturing the intended stable relationships and the synchronization of related objects. We prove that the original OCPNs and the resulting OPIDs coincide for those executions that satisfy the intended relationships. Moreover, we provide an implementation of the mapping from OCPN to OPID under stable relationships.

2025-08-18T18:10:27Z Anjo Seidel Sarah Winkler Alessandro Gianola Marco Montali Mathias Weske http://arxiv.org/abs/2508.12620v1 2025-08-18T04:33:03Z

Large language models (LLMs) have recently shown impressive results on diverse code-related tasks, benefiting from large-scale training and instruction tuning. However, studies reveal that their grasp of fundamental programming concepts, such as data flow and control flow, remains shallow, leading to fragile performance when code requires deeper reasoning. This limitation restricts the practical adoption of LLMs in real-world software development. To address this issue, this work introduces a counterfactual code augmentation framework combined with concept-aware tuning, designed to guide LLMs toward stronger conceptual understanding. Comprehensive evaluation across multiple models and benchmarks demonstrates the effectiveness of the proposed approach.

2025-08-18T04:33:03Z 11 pages, 7 figures Xiaoning Ren Qiang Hu Wei Ma Yan Li Yao Zhang Lingxiao Jiang Yinxing Xue http://arxiv.org/abs/2508.12475v1 2025-08-17T19:34:24Z

Prompt programming treats large language model prompts as software components with typed interfaces. Based on a literature survey of 15 recent works from 2023 to 2025, we observe a consistent trend: type systems are central to emerging prompt programming frameworks. However, there are gaps in constraint expressiveness and in supporting algorithms. To address these issues, we introduce the notion of Lambda Prompt, a dependently typed calculus with probabilistic refinements for syntactic and semantic constraints. While this is not yet a full calculus, the formulation motivates a type-theoretic foundation for prompt programming. Our catalog of 13 constraints highlights underexplored areas in constraint expressiveness (constraints 9 through 13). To address the algorithmic gap, we propose a constraint-preserving optimization rule. Finally, we outline research directions on developing a compiler for prompt programs.

2025-08-17T19:34:24Z Accepted as Extended Abstract in TyDe Workshop 2025,co-located with ICFP Abhijit Paul http://arxiv.org/abs/2508.12427v1 2025-08-17T16:44:50Z

Copatterns give functional programs a flexible mechanism for responding to their context, and composition can greatly enhance their expressiveness. However, that same expressive power makes it harder to precisely specify the behavior of programs. Using Danvy's functional and syntactic correspondence between different semantic artifacts, we derive a full suite of semantics for copatterns, twice. First, a calculus of monolithic copatterns is taken on a journey from small-step operational semantics to abstract machine to continuation-passing style. Then within continuation-passing style, we refactor the semantics to derive a more general calculus of compositional copatterns, and take the return journey back to derive the other semantic artifacts in reverse order.

2025-08-17T16:44:50Z To find the detailed step-by-step process, which serves as their proof of correctness, see https://github.com/pdownen/derive-copat Paul Downen 10.1145/3759427.3760362 http://arxiv.org/abs/2508.12054v1 2025-08-16T14:12:55Z

In his 1984 Turing Award lecture, Ken Thompson showed that a compiler could be maliciously altered to insert backdoors into programs it compiles and perpetuate this behavior by modifying any compiler it subsequently builds. Thompson's hack has been reproduced in real-world systems for demonstration purposes. Several countermeasures have been proposed to defend against Thompson-style backdoors, including the well-known {\it Diverse Double-Compiling} (DDC) technique, as well as methods like translation validation and CompCert-style compilation. However, these approaches ultimately circle back to the fundamental question: "How can we trust the compiler used to compile the tools we rely on?" In this paper, we introduce a novel approach to generating certificates to guarantee that a binary image faithfully represents the source code. These certificates ensure that the binary contains all and only the statements from the source code, preserves their order, and maintains equivalent def-use dependencies. The certificate is represented as an integer derivable from both the source code and the binary using a concise set of derivation rules, each applied in constant time. To demonstrate the practicality of our method, we present Charon, a compiler designed to handle a subset of C expressive enough to compile FaCT, the Flexible and Constant Time cryptographic programming language.

2025-08-16T14:12:55Z 32 pages, 19 figures Guilherme de Oliveira Silva Fernando Magno Quintão Pereira http://arxiv.org/abs/2508.11451v1 2025-08-15T12:59:10Z

Compute-Near-Memory (CNM) systems offer a promising approach to mitigate the von Neumann bottleneck by bringing computational units closer to data. However, optimizing for these architectures remains challenging due to their unique hardware and programming models. Existing CNM compilers often rely on manual programmer annotations for offloading and optimizations. Automating these decisions by exploring the optimization space, common in CPU/GPU systems, is difficult for CNMs as constructing and navigating the transformation space is tedious and time consuming. This is particularly the case during system-level design, where evaluation requires time-consuming simulations. To address this, we present CoMoNM, a generic cost modeling framework for CNM systems for execution time estimation in milliseconds. It takes a high-level, hardware-agnostic application representation, target system specifications, and a mapping specification as input and estimates the execution time for the given application on the target CNM system. We show how CoMoNM can be seamlessly integrated into state-of-the-art CNM compilers, providing improved offloading decisions. Evaluation on established benchmarks for CNM shows estimation errors within 7.80% and 2.99%, when compared to the real UPMEM CNM system and Samsung's HBM-PIM simulator. Notably, CoMoNM delivers estimates seven orders of magnitude faster compared to the UPMEM and HBM-PIM simulators.

2025-08-15T12:59:10Z 12 pages, 16 Figures Hamid Farzaneh Asif Ali Khan Jeronimo Castrillon http://arxiv.org/abs/2508.11443v1 2025-08-15T12:48:32Z

We present a systematic derivation of a data-parallel implementation of two-level, static and collision-free hash maps, by giving a functional formulation of the Fredman et al. construction, and then flattening it. We discuss the challenges of providing a flexible, polymorphic, and abstract interface to hash maps in a functional array language, with particular attention paid to the problem of dynamically sized keys, which we address by associating each hash map with an arbitrary context. The algorithm is implemented in Futhark, and the achieved GPU execution performance is compared on simple benchmark problems. We find that our hash maps outperform conventional tree/search-based approaches. Furthermore, our implementation is compared against the state-of-the-art cuCollections library, which is significantly faster for hash map construction, and to a lesser degree for lookups. We explain to which extent the performance difference is due to low-level code generation limitation in the Futhark compiler, and to which extent it can be attributed to the data-parallel programming vocabulary not providing the constructs necessary to express the equivalent of the algorithms used by cuCollections. We end by reflecting to which extent the functional array language programming model could, or should, be extended to address these weaknesses.

2025-08-15T12:48:32Z William Henrich Due Martin Elsman Troels Henriksen http://arxiv.org/abs/2508.11297v1 2025-08-15T08:04:46Z

Reduction-based interpreters are traditionally defined in terms of a one-step reduction function which systematically decomposes a term into a potential redex and context, contracts the redex, and recomposes it to construct the new term to be further reduced. While implementing such interpreters follows a systematic recipe, they often require interpreter engineers to write a substantial amount of code -- much of it boilerplate. In this paper, we apply well-known techniques from generic programming to reduce boilerplate code in reduction-based interpreters.

2025-08-15T08:04:46Z Casper Bach http://arxiv.org/abs/2403.08173v3 2025-08-14T13:16:30Z

We present a novel characterization of stable mergesort functions using relational parametricity, and show that it implies the functional correctness of mergesort. As a result, one can prove the correctness of several variations of mergesort (e.g., top-down, bottom-up, tail-recursive, non-tail-recursive, smooth, and non-smooth mergesorts) by proving the characteristic property for each variation. Thanks to our characterization and the parametricity translation, we deduced the correctness results, including stability, of various implementations of mergesort for lists, including highly optimized ones, in the Rocq Prover (formerly the Coq Proof Assistant).

2024-03-13T01:54:33Z Extended version of the ICFP'25 paper Proc. ACM Program. Lang. 9, ICFP, Article 236 (August 2025) Cyril Cohen Kazuhiko Sakaguchi 10.1145/3747505 http://arxiv.org/abs/2505.15002v2 2025-08-13T21:59:23Z

Combinatory Homomorphic Automatic Differentiation (CHAD) was originally formulated as a semantics-driven source-to-source transformation for reverse-mode AD of total (terminating) functional programs. In this work, we extend CHAD to encompass programs featuring constructs such as partial (potentially non-terminating) operations, data-dependent conditionals (e.g., real-valued tests), and iteration constructs (i.e. while-loops), while maintaining CHAD's core principle of structure-preserving semantics. A central contribution is the introduction of iteration-extensive indexed categories, which provide a principled integration of iteration into dependently typed programming languages. This integration is achieved by requiring that iteration in the base category lifts to parameterized initial algebras in the indexed category, yielding an op-fibred iterative structure that models while-loops and other iteration constructs in the total category, which corresponds to the category of containers of our dependently typed language. Through the idea of iteration-extensive indexed categories, we extend the CHAD transformation to looping programs as the unique structure-preserving functor in a suitable sense. Specifically, it is the unique iterative Freyd category morphism from the iterative Freyd category corresponding to the source language to the category of containers obtained from the target language, such that each primitive operation is mapped to its (transposed) derivative. We establish the correctness of this extended transformation via the universal property of the syntactic categorical model of the source language, showing that the differentiated programs compute correct reverse-mode derivatives of their originals.

2025-05-21T01:10:40Z 58 pages Fernando Lucatelli Nunes Gordon Plotkin Matthijs Vákár