https://arxiv.org/api/ljxeZaBG43Clp86RYl7MA/4QRpo 2026-06-30T18:34:26Z 9958 1980 15 http://arxiv.org/abs/2412.06874v1 2024-12-09T16:08:22Z

The rapid growth of the travel industry has increased the need for real-time optimization in reservation systems that could take care of huge data and transaction volumes. This study proposes a hybrid framework that ut folds an Artificial Intelligence and a Microservices approach for the performance optimization of the system. The AI algorithms forecast demand patterns, optimize the allocation of resources, and enhance decision-making driven by Microservices architecture, hence decentralizing system components for scalability, fault tolerance, and reduced downtime. The model provided focuses on major problems associated with the travel reservation systems such as latency of systems, load balancing and data consistency. It endows the systems with predictive models based on AI improved ability to forecast user demands. Microservices would also take care of different scales during uneven traffic patterns. Hence, both aspects ensure better handling of peak loads and spikes while minimizing delays and ensuring high service quality. A comparison was made between traditional reservation models, which are monolithic and the new model of AI-Microservices. Comparatively, the analysis results state that there is a drastic improvement in processing times where the system uptime and resource utilization proved the capability of AI and the microservices in transforming the travel industry in terms of reservation. This research work focused on AI and Microservices towards real-time optimization, providing critical insight into how to move forward with practical recommendations for upgrading travel reservation systems with this technology.

2024-12-09T16:08:22Z 19 pages, 12 figures Biman Barua M. Shamim Kaiser http://arxiv.org/abs/2412.06391v1 2024-12-09T11:18:14Z

In this paper, we present the design of Owi, a symbolic interpreter for WebAssembly written in OCaml, and how we used it to create a state-of-the-art tool to find bugs in programs combining C and Rust code. WebAssembly (Wasm) is a binary format for executable programs. Originally intended for web applications, Wasm is also considered a serious alternative for server-side runtimes and embedded systems due to its performance and security benefits. Despite its security guarantees and sandboxing capabilities, Wasm code is still vulnerable to buffer overflows and memory leaks, which can lead to exploits on production software. To help prevent those, different techniques can be used, including symbolic execution. Owi is built around a modular, monadic interpreter capable of both normal and symbolic execution of Wasm programs. Monads have been identified as a way to write modular interpreters since 1995 and this strategy has allowed us to build a robust and performant symbolic execution tool which our evaluation shows to be the best currently available for Wasm. Moreover, because WebAssembly is a compilation target for multiple languages (such as Rust and C), Owi can be used to find bugs in C and Rust code, as well as in codebases mixing the two. We demonstrate this flexibility through illustrative examples and evaluate its scalability via comprehensive experiments using the 2024 Test-Comp benchmarks. Results show that Owi achieves comparable performance to state-of-the-art tools like KLEE and Symbiotic, and exhibits advantages in specific scenarios where KLEE's approximations could lead to false negatives.

2024-12-09T11:18:14Z The Art, Science, and Engineering of Programming, 2025, Vol. 9, Issue 1, Article 3 Léo Andrès OCamlPro, France / Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - LMF, France Filipe Marques INESC-ID, Portugal / University of Lisbon, Portugal Arthur Carcano OCamlPro, France Pierre Chambart OCamlPro, France José Fragoso Santos INESC-ID, Portugal / University of Lisbon, Portugal Jean-Christophe Filliâtre Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - LMF, France 10.22152/programming-journal.org/2025/9/3 http://arxiv.org/abs/2412.06274v1 2024-12-09T07:48:15Z

Live programming features can be found in a range of programming environments, from individual prototypes to widely used environments. While liveness is generally considered a useful property, there is little empirical evidence on when and how liveness can be beneficial. Even though there are few experimental studies, their results are largely inconclusive. We reviewed existing experiments and related studies to gather a collection of potential effects of liveness and moderating factors. Based on this collection, we concluded that **task complexity** and **prior experience addressing liveness** are potentially essential factors neglected in previous experiments. To fill this gap, we devised and conducted a controlled experiment (N = 37) testing the hypothesis that task complexity moderates the effects of live introspection tools on participants? debugging efficiency, given participants with prior experience with liveness. Our results do not support the hypothesis that task complexity moderates the effect of live introspection tools. This non-significant moderation effect might result from the low number of participants, as the data suggests a moderation effect. The results also show that in our experiment setting, live introspection tools significantly reduced the time participants took to debug the tasks. For researchers interested in the effects of liveness, our findings suggest that studies on liveness should make conscious choices about task complexity and participants' prior experience with liveness. For designers of programming environments, the results of our experiment are a step toward understanding when and how programming tools should be live to become more helpful to programmers.

2024-12-09T07:48:15Z The Art, Science, and Engineering of Programming, 2025, Vol. 9, Issue 1, Article 1 Patrick Rein Hasso Plattner Institute, Germany / University of Potsdam, Germany Stefan Ramson Hasso Plattner Institute, Germany / University of Potsdam, Germany Tom Beckmann Hasso Plattner Institute, Germany / University of Potsdam, Germany Robert Hirschfeld Hasso Plattner Institute, Germany / University of Potsdam, Germany 10.22152/programming-journal.org/2025/9/1 http://arxiv.org/abs/2412.06269v1 2024-12-09T07:42:35Z

Many improvements to programming have come from shortening feedback loops, for example with Integrated Development Environments, Unit Testing, Live Programming, and Distributed Version Control. A barrier to feedback that deserves greater attention is Schema Evolution. When requirements on the shape of data change then existing data must be migrated into the new shape, and existing code must be modified to suit. Currently these adaptations are often performed manually, or with ad hoc scripts. Manual schema evolution not only delays feedback but since it occurs outside the purview of version control tools it also interrupts collaboration. Schema evolution has long been studied in databases. We observe that the problem also occurs in non-database contexts that have been less studied. We present a suite of challenge problems exemplifying this range of contexts, including traditional database programming as well as live front-end programming, model-driven development, and collaboration in computational documents. We systematize these various contexts by defining a set of layers and dimensions of schema evolution. We offer these challenge problems to ground future research on the general problem of schema evolution in interactive programming systems and to serve as a basis for evaluating the results of that research. We hope that better support for schema evolution will make programming more live and collaboration more fluid.

2024-12-09T07:42:35Z arXiv admin note: text overlap with arXiv:2309.11406 The Art, Science, and Engineering of Programming, 2025, Vol. 9, Issue 1, Article 2 Jonathan Edwards Independent, USA Tomas Petricek Charles University, Czechia Tijs van der Storm CWI, Netherlands / University of Groningen, Netherlands Geoffrey Litt Ink & Switch, USA 10.22152/programming-journal.org/2025/9/2 http://arxiv.org/abs/2412.06102v1 2024-12-08T23:17:19Z

Document databases are increasingly popular in various applications, but their queries are challenging to write due to the flexible and complex data model underlying document databases. This paper presents a synthesis technique that aims to generate document database queries from input-output examples automatically. A new domain-specific language is designed to express a representative set of document database queries in an algebraic style. Furthermore, the synthesis technique leverages a novel abstraction of collections for deduction to efficiently prune the search space and quickly generate the target query. An evaluation of 110 benchmarks from various sources shows that the proposed technique can synthesize 108 benchmarks successfully. On average, the synthesizer can generate document database queries from a small number of input-output examples within tens of seconds.

2024-12-08T23:17:19Z Qikang Liu Yang He Yanwen Cai Byeongguk Kwak Yuepeng Wang http://arxiv.org/abs/2404.04837v3 2024-12-07T21:21:53Z

Categories and categorical structures are increasingly recognized as useful abstractions for modeling in science and engineering. To uniformly implement category-theoretic mathematical models in software, we introduce GATlab, a domain-specific language for algebraic specification embedded in a technical programming language. GATlab is based on generalized algebraic theories (GATs), a logical system extending algebraic theories with dependent types so as to encompass category theory. Using GATlab, the programmer can specify generalized algebraic theories and their models, including both free models, based on symbolic expressions, and computational models, defined by arbitrary code in the host language. Moreover, the programmer can define maps between theories and use them to declaratively migrate models of one theory to models of another. In short, GATlab aims to provide a unified environment for both computer algebra and software interface design with generalized algebraic theories. In this paper, we describe the design, implementation, and applications of GATlab.

2024-04-07T07:11:29Z 14 pages plus references and appendix. To appear at MFPS 2024 Electronic Notes in Theoretical Informatics and Computer Science, Volume 4 - Proceedings of MFPS XL (December 11, 2024) entics:14666 Owen Lynch Kris Brown James Fairbanks Evan Patterson 10.46298/entics.14666 http://arxiv.org/abs/2404.03825v3 2024-12-07T21:04:56Z

Parametricity is a key metatheoretic property of type systems, which implies strong uniformity & modularity properties of the structure of types within systems possessing it. In recent years, various systems of dependent type theory have emerged with the aim of expressing such parametric reasoning in their internal logic, toward the end of solving various problems arising from the complexity of higher-dimensional coherence conditions in type theory. This paper presents a first step toward the unification, simplification, and extension of these various methods for internalizing parametricity. Specifically, I argue that there is an essentially modal aspect of parametricity, which is intimately connected with the category-theoretic concept of cohesion. On this basis, I describe a general categorical semantics for modal parametricity, develop a corresponding framework of axioms (with computational interpretations) in dependent type theory that can be used to internally represent and reason about such parametricity, and show this in practice by implementing these axioms in Agda and using them to verify parametricity theorems therein. I then demonstrate the utility of these axioms in managing the complexity of higher-dimensional coherence by deriving induction principles for higher inductive types, and in closing, I sketch the outlines of a more general synthetic theory of parametricity, with applications in domains ranging from homotopy type theory to the analysis of program modules.

2024-04-04T22:57:42Z Electronic Notes in Theoretical Informatics and Computer Science, Volume 4 - Proceedings of MFPS XL (December 11, 2024) entics:14710 C. B. Aberlé 10.46298/entics.14710 http://arxiv.org/abs/2404.00212v4 2024-12-07T20:58:23Z

We study a cost-aware programming language for higher-order recursion dubbed $\textbf{PCF}_\mathsf{cost}$ in the setting of synthetic domain theory (SDT). Our main contribution relates the denotational cost semantics of $\textbf{PCF}_\mathsf{cost}$ to its computational cost semantics, a new kind of dynamic semantics for program execution that serves as a mathematically natural alternative to operational semantics in SDT. In particular we prove an internal, cost-sensitive version of Plotkin's computational adequacy theorem, giving a precise correspondence between the denotational and computational semantics for complete programs at base type. The constructions and proofs of this paper take place in the internal dependent type theory of an SDT topos extended by a phase distinction in the sense of Sterling and Harper. By controlling the interpretation of cost structure via the phase distinction in the denotational semantics, we show that $\textbf{PCF}_\mathsf{cost}$ programs also evince a noninterference property of cost and behavior. We verify the axioms of the type theory by means of a model construction based on relative sheaf models of SDT.

2024-03-30T01:37:23Z Final version for MFPS '24 Electronic Notes in Theoretical Informatics and Computer Science, Volume 4 - Proceedings of MFPS XL (December 11, 2024) entics:14732 Yue Niu Jonathan Sterling Robert Harper 10.46298/entics.14732 http://arxiv.org/abs/2411.07714v2 2024-12-07T20:51:48Z

We consider the problem of designing typed concurrent calculi with non-deterministic choice in which types leverage linearity for controlling resources, thereby ensuring strong correctness properties for processes. This problem is constrained by the delicate tension between non-determinism and linearity. Prior work developed a session-typed π-calculus with standard non-deterministic choice; well-typed processes enjoy type preservation and deadlock-freedom. Central to this typed calculus is a lazy semantics that gradually discards branches in choices. This lazy semantics, however, is complex: various technical elements are needed to describe the non-deterministic behavior of typed processes. This paper develops an entirely new approach, based on an eager semantics, which more directly represents choices and commitment. We present a π-calculus in which non-deterministic choices are governed by this eager semantics and session types. We establish its key correctness properties, including deadlock-freedom, and demonstrate its expressivity by correctly translating a typed resource λ-calculus.

2024-11-12T11:03:02Z arXiv admin note: substantial text overlap with arXiv:2408.07915 Electronic Notes in Theoretical Informatics and Computer Science, Volume 4 - Proceedings of MFPS XL (December 11, 2024) entics:14735 Bas van den Heuvel Daniele Nantes-Sobrinho Joseph W. N. Paulus Jorge A. Pérez 10.46298/entics.14735 http://arxiv.org/abs/2411.09489v2 2024-12-07T20:41:31Z

Recently, Miller and Wu introduced the positive $λ$-calculus, a call-by-value $λ$-calculus with sharing obtained by assigning proof terms to the positively polarized focused proofs for minimal intuitionistic logic. The positive $λ$-calculus stands out among $λ$-calculi with sharing for a compactness property related to the sharing of variables. We show that -- thanks to compactness -- the positive calculus neatly captures the core of useful sharing, a technique for the study of reasonable time cost models.

2024-11-14T14:51:43Z Paper for the proceedings of MFPS 2024 Electronic Notes in Theoretical Informatics and Computer Science, Volume 4 - Proceedings of MFPS XL (December 11, 2024) entics:14758 Beniamino Accattoli Jui-Hsuan Wu 10.46298/entics.14758 http://arxiv.org/abs/2404.03641v4 2024-12-07T20:34:43Z

Amortized analysis is a cost analysis technique for data structures in which cost is studied in aggregate: rather than considering the maximum cost of a single operation, one bounds the total cost encountered throughout a session. Traditionally, amortized analysis has been phrased inductively, quantifying over finite sequences of operations. Connecting to prior work on coalgebraic semantics for data structures, we develop the alternative perspective that amortized analysis is naturally viewed coalgebraically in a category of cost algebras, where a morphism of coalgebras serves as a first-class generalization of potential function suitable for integrating cost and behavior. Using this simple definition, we consider amortization of other sample effects, non-commutative printing and randomization. To support imprecise amortized upper bounds, we adapt our discussion to the bicategorical setting, where a potential function is a colax morphism of coalgebras. We support algebraic and coalgebraic operations simultaneously by using coalgebras for an endoprofunctor instead of an endofunctor, combining potential using a monoidal structure on the underlying category. Finally, we compose amortization arguments in the indexed category of coalgebras to implement one amortized data structure in terms of others.

2024-04-04T17:57:22Z Electronic Notes in Theoretical Informatics and Computer Science, Volume 4 - Proceedings of MFPS XL (December 11, 2024) entics:14797 Harrison Grodin Robert Harper 10.46298/entics.14797 http://arxiv.org/abs/2412.05496v1 2024-12-07T01:46:38Z

Over the past 7 years, attention has become one of the most important primitives in deep learning. The primary approach to optimize attention is FlashAttention, which fuses the operation together, drastically improving both the runtime and the memory consumption. However, the importance of FlashAttention combined with its monolithic nature poses a problem for researchers aiming to try new attention variants -- a "software lottery". This problem is exacerbated by the difficulty of writing efficient fused attention kernels, resisting traditional compiler-based approaches. We introduce FlexAttention, a novel compiler-driven programming model that allows implementing the majority of attention variants in a few lines of idiomatic PyTorch code. We demonstrate that many existing attention variants (e.g. Alibi, Document Masking, PagedAttention, etc.) can be implemented via FlexAttention, and that we achieve competitive performance compared to these handwritten kernels. Finally, we demonstrate how FlexAttention allows for easy composition of attention variants, solving the combinatorial explosion of attention variants.

2024-12-07T01:46:38Z Juechu Dong Boyuan Feng Driss Guessous Yanbo Liang Horace He http://arxiv.org/abs/2309.06913v3 2024-12-06T16:34:49Z

Various categories have been proposed as targets for the denotational semantics of higher-order probabilistic programming languages. One such proposal involves joint probability distributions (couplings) used in Bayesian statistical models with conditioning. In previous treatments, composition of joint measures was performed by disintegrating to obtain Markov kernels, composing the kernels, then reintegrating to obtain a joint measure. Disintegrations exist only under certain restrictions on the underlying spaces. In this paper we propose a category whose morphisms are joint finite measures in which composition is defined without reference to disintegration, allowing its application to a broader class of spaces. The category is symmetric monoidal with a pleasing symmetry in which the dagger structure is a simple transpose.

2023-09-13T12:24:09Z 14 pages, MFPS 2023 Electronic Notes in Theoretical Informatics and Computer Science, Volume 3 - Proceedings of MFPS XXXIX (November 23, 2023) entics:12279 Dexter Kozen Alexandra Silva Erik Voogd 10.46298/entics.12279 http://arxiv.org/abs/2207.02502v2 2024-12-06T13:47:09Z

Distributed systems adopt weak consistency to ensure high availability and low latency, but state convergence is hard to guarantee due to conflicts. Experts carefully design replicated data types (RDTs) that resemble sequential data types and embed conflict resolution mechanisms that ensure convergence. Designing RDTs is challenging as their correctness depends on subtleties such as the ordering of concurrent operations. Currently, researchers manually verify RDTs, either by paper proofs or using proof assistants. Unfortunately, paper proofs are subject to reasoning flaws and mechanized proofs verify a formalisation instead of a real-world implementation. Furthermore, writing mechanized proofs is reserved to verification experts and is extremely time consuming. To simplify the design, implementation, and verification of RDTs, we propose VeriFx, a high-level programming language with automated proof capabilities. VeriFx lets programmers implement RDTs atop functional collections and express correctness properties that are verified automatically. Verified RDTs can be transpiled to mainstream languages (currently Scala or JavaScript). VeriFx also provides libraries for implementing and verifying Conflict-free Replicated Data Types (CRDTs) and Operational Transformation (OT) functions. These libraries implement the general execution model of those approaches and define their correctness properties. We use the libraries to implement and verify an extensive portfolio of 35 CRDTs and reproduce a study on the correctness of OT functions.

2022-07-06T08:11:12Z 35 pages, 13 figures Kevin De Porre Carla Ferreira Elisa Gonzalez Boix http://arxiv.org/abs/2411.14174v2 2024-12-06T04:14:08Z

Rust aims to offer full memory safety for programs, a guarantee that untamed C programs do not enjoy. How difficult is it to translate existing C code to Rust? To get a complementary view from that of automatic C to Rust translators, we report on a user study asking humans to translate real-world C programs to Rust. Our participants are able to produce safe Rust translations, whereas state-of-the-art automatic tools are not able to do so. Our analysis highlights that the high-level strategy taken by users departs significantly from those of automatic tools we study. We also find that users often choose zero-cost (static) abstractions for temporal safety, which addresses a predominant component of runtime costs in other full memory safety defenses. User-provided translations showcase a rich landscape of specialized strategies to translate the same C program in different ways to safe Rust, which future automatic translators can consider.

2024-11-21T14:37:05Z Accepted by NDSS Symposium 2025. Please cite the conference version of this paper, e.g., "Ruishi Li, Bo Wang, Tianyu Li, Prateek Saxena, Ashish Kundu. Translating C To Rust: Lessons from a User Study. In 32nd Annual Network and Distributed System Security Symposium (NDSS 2025)." Ruishi Li Bo Wang Tianyu Li Prateek Saxena Ashish Kundu 10.14722/ndss.2025.241407