https://arxiv.org/api/i80gPfEI9Pa6QdsWCQVu9AYNwNs 2026-06-30T05:47:39Z 9958 1785 15 http://arxiv.org/abs/2410.07295v2 IterGen: Iterative Semantic-aware Structured LLM Generation with Backtracking 2025-03-02T01:39:57Z Large Language Models (LLMs) are widely used for tasks such as natural language and code generation, but their outputs often suffer from issues like hallucination, toxicity, and incorrect results. Current libraries for structured LLM generation rely on left-to-right decoding without support for backtracking, limiting the ability to correct or refine outputs mid-generation. To address this, we introduce IterGen, a user-friendly library for iterative, grammar-guided LLM generation that enables users to move both forward and backward within the generated output based on grammar symbols. By leveraging a symbol-to-position mapping and maintaining the key-value (KV) cache state, IterGen ensures efficient and structured generation while allowing for corrections during the process. We demonstrate IterGen's effectiveness in two important applications: reducing privacy leakage in LLM outputs and improving the accuracy of LLM-generated SQL and Vega-Lite queries. Our code and additional resources are available at https://structuredllm.com. 2024-10-09T16:21:38Z Accepted at ICLR 2025 Shubham Ugare Rohan Gumaste Tarun Suresh Gagandeep Singh Sasa Misailovic http://arxiv.org/abs/2406.04604v4 Learning Task Decomposition to Assist Humans in Competitive Programming 2025-03-01T20:47:54Z When using language models (LMs) to solve complex problems, humans might struggle to understand the LM-generated solutions and repair the flawed ones. To assist humans in repairing them, we propose to automatically decompose complex solutions into multiple simpler pieces that correspond to specific subtasks. We introduce a novel objective for learning task decomposition, termed assistive value (AssistV), which measures the feasibility and speed for humans to repair the decomposed solution. We collect a dataset of human repair experiences on different decomposed solutions. Utilizing the collected data as in-context examples, we then learn to critique, refine, and rank decomposed solutions to improve AssistV. We validate our method under competitive programming problems: under 177 hours of human study, our method enables non-experts to solve 33.3\% more problems, speeds them up by 3.3x, and empowers them to match unassisted experts. 2024-06-07T03:27:51Z ACL 2024 Main Conference Jiaxin Wen Ruiqi Zhong Pei Ke Zhihong Shao Hongning Wang Minlie Huang http://arxiv.org/abs/2405.03058v6 A Unified Framework for Automated Code Transformation and Pragma Insertion 2025-03-01T05:43:19Z High-level synthesis, source-to-source compilers, and various Design Space Exploration techniques for pragma insertion have significantly improved the Quality of Results of generated designs. These tools offer benefits such as reduced development time and enhanced performance. However, achieving high-quality results often requires additional manual code transformations and tiling selections, which are typically performed separately or as pre-processing steps. Although DSE techniques enable code transformation upfront, the vastness of the search space often limits the exploration of all possible code transformations, making it challenging to determine which transformations are necessary. Additionally, ensuring correctness remains challenging, especially for complex transformations and optimizations. To tackle this obstacle, we first propose a comprehensive framework leveraging HLS compilers. Our system streamlines code transformation, pragma insertion, and tiles size selection for on-chip data caching through a unified optimization problem, aiming to enhance parallelization, particularly beneficial for computation-bound kernels. Them employing a novel Non-Linear Programming (NLP) approach, we simultaneously ascertain transformations, pragmas, and tile sizes, focusing on regular loop-based kernels. Our evaluation demonstrates that our framework adeptly identifies the appropriate transformations, including scenarios where no transformation is necessary, and inserts pragmas to achieve a favorable Quality of Results. 2024-05-05T21:41:43Z Stéphane Pouget Louis-Noël Pouchet Jason Cong 10.1145/3706628.3708873 http://arxiv.org/abs/2211.07117v3 Unrealizability Logic 2025-03-01T04:27:03Z We consider the problem of establishing that a program-synthesis problem is unrealizable (i.e., has no solution in a given search space of programs). Prior work on unrealizability has developed some automatic techniques to establish that a problem is unrealizable; however, these techniques are all black-box, meaning that they conceal the reasoning behind why a synthesis problem is unrealizable. In this paper, we present a Hoare-style reasoning system, called unrealizability logic for establishing that a program-synthesis problem is unrealizable. To the best of our knowledge, unrealizability logic is the first proof system for overapproximating the execution of an infinite set of imperative programs. The logic provides a general, logical system for building checkable proofs about unrealizability. Similar to how Hoare logic distills the fundamental concepts behind algorithms and tools to prove the correctness of programs, unrealizability logic distills into a single logical system the fundamental concepts that were hidden within prior tools capable of establishing that a program-synthesis problem is unrealizable. 2022-11-14T05:11:47Z Jinwoo Kim Loris D'Antoni Thomas Reps 10.1145/3571216 http://arxiv.org/abs/2502.21053v1 Proof systems for partial incorrectness logic (partial reverse Hoare logic) 2025-02-28T13:51:09Z Partial incorrectness logic (partial reverse Hoare logic) has recently been introduced as a new Hoare-style logic that over-approximates the weakest pre-conditions of a program and a post-condition. It is expected to verify systems where the final state must guarantee its initial state, such as authentication, secure communication tools and digital signatures. However, the logic has only been given semantics. This paper defines two proof systems for partial incorrectness logic (partial reverse Hoare logic): ordinary and cyclic proof systems. They are sound and relatively complete. The relative completeness of our ordinary proof system is proved by showing that the weakest pre-condition of a while loop and a post-condition is its loop invariant. The relative completeness of our cyclic proof system is also proved by providing a way to transform any cyclic proof into an ordinary proof. 2025-02-28T13:51:09Z 23 pages Yukihiro Oda http://arxiv.org/abs/2502.20547v1 An Attempt to Catch Up with JIT Compilers: The False Lead of Optimizing Inline Caches 2025-02-27T21:42:49Z Context: Just-in-Time (JIT) compilers are able to specialize the code they generate according to a continuous profiling of the running programs. This gives them an advantage when compared to Ahead-of-Time (AoT) compilers that must choose the code to generate once for all. Inquiry: Is it possible to improve the performance of AoT compilers by adding Dynamic Binary Modification (DBM) to the executions? Approach: We added to the Hopc AoT JavaScript compiler a new optimization based on DBM to the inline cache (IC), a classical optimization dynamic languages use to implement object property accesses efficiently. Knowledge: Reducing the number of memory accesses as the new optimization does, does not shorten execution times on contemporary architectures. Grounding: The DBM optimization we have implemented is fully operational on x86_64 architectures. We have conducted several experiments to evaluate its impact on performance and to study the reasons of the lack of acceleration. Importance: The (negative) result we present in this paper sheds new light on the best strategy to be used to implement dynamic languages. It tells that the old days were removing instructions or removing memory reads always yielded to speed up is over. Nowadays, implementing sophisticated compiler optimizations is only worth the effort if the processor is not able by itself to accelerate the code. This result applies to AoT compilers as well as JIT compilers. 2025-02-27T21:42:49Z The Art, Science, and Engineering of Programming, 2025, Vol. 10, Issue 1, Article 6 Aurore Poirier University of Rennes - Inria - CNRS - IRISA, France Erven Rohou University of Rennes - Inria - CNRS - IRISA, France Manuel Serrano Inria - University of Côte d'Azur, France 10.22152/programming-journal.org/2026/10/6 http://arxiv.org/abs/2502.20546v1 On the State of Coherence in the Land of Type Classes 2025-02-27T21:42:04Z Type classes are a popular tool for implementing generic algorithms and data structures without loss of efficiency, bridging the gap between parametric and ad-hoc polymorphism. Since their initial development in Haskell, they now feature prominently in numerous other industry-ready programming languages, notably including Swift, Rust, and Scala. The success of type classes hinges in large part on the compilers' ability to infer arguments to implicit parameters by means of a type-directed resolution. This technique, sometimes dubbed **implicit programming**, lets users elide information that the language implementation can deduce from the context, such as the implementation of a particular type class. One drawback of implicit programming is that a type-directed resolution may yield ambiguous results, thereby threatening coherence, the property that valid programs have exactly one meaning. This issue has divided the community on the right approach to address it. One side advocates for flexibility where implicit resolution is context-sensitive and often relies on dependent typing features to uphold soundness. The other holds that context should not stand in the way of equational reasoning and typically imposes that type class instances be unique across the entire program to fend off ambiguities. Although there exists a large body of work on type classes and implicit programming, most of the scholarly literature focuses on a few select languages and offers little insight into other mainstream projects. Meanwhile, the latter have evolved similar features and/or restrictions under different names, making it difficult for language users and designers to get a sense of the full design space. To alleviate this issue, we set to examine Swift, Rust, and Scala, three popular languages featuring type classes heavily, and relate their approach to coherence to Haskell's. It turns out that, beyond superficial syntactic differences, Swift, Rust, and Haskell are actually strikingly similar in that the three languages offer comparable strategies to work around the limitations of the uniqueness of type class instances. 2025-02-27T21:42:04Z The Art, Science, and Engineering of Programming, 2025, Vol. 10, Issue 1, Article 15 Dimi Racordon EPFL, Switzerland Eugene Flesselle EPFL, Switzerland Cao Nguyen Pham EPFL, Switzerland 10.22152/programming-journal.org/2026/10/15 http://arxiv.org/abs/2502.20543v1 Meta-compilation of Baseline JIT Compilers with Druid 2025-02-27T21:41:07Z Virtual Machines (VMs) combine interpreters and just-in-time (JIT) compiled code to achieve good performance. However, implementing different execution engines increases the cost of developing and maintaining such solutions. JIT compilers based on meta-compilation cope with these issues by automatically generating optimizing JIT compilers. This leaves open the question of how meta-compilation applies to baseline JIT compilers, which improve warmup times by trading off optimizations. In this paper, we present Druid, an ahead-of-time automatic approach to generate baseline JIT compiler frontends from interpreters. Language developers guide meta-compilation by annotating interpreter code and using Druid's intrinsics. Druid targets the meta-compilation to an existing JIT compiler infrastructure to achieve good warm-up performance. We applied Druid in the context of the Pharo programming language and evaluated it by comparing an autogenerated JIT compiler frontend against the one in production for more than 10 years. Our generated JIT compiler frontend is 2x faster on average than the interpreter and achieves on average 0.7x the performance of the handwritten JIT compiler. Our experiment only required changes in 60 call sites in the interpreter, showing that our solution makes language VMs **easier to maintain and evolve in the long run**. 2025-02-27T21:41:07Z The Art, Science, and Engineering of Programming, 2025, Vol. 10, Issue 1, Article 9 Nahuel Palumbo University of Lille - Inria - CNRS - Centrale Lille - UMR 9189 CRIStAL, France Guillermo Polito University of Lille - Inria - CNRS - Centrale Lille - UMR 9189 CRIStAL, France Stéphane Ducasse University of Lille - Inria - CNRS - Centrale Lille - UMR 9189 CRIStAL, France Pablo Tesone University of Lille - Inria - CNRS - Centrale Lille - UMR 9189 CRIStAL, France 10.22152/programming-journal.org/2026/10/9 http://arxiv.org/abs/2502.20542v1 Conversational Concurrency with Dataspaces and Facets 2025-02-27T21:40:47Z Context: Developers have come to appreciate the simplicity of message-passing actors for concurrent programming tasks. The actor model of computation is easy to grasp; it is just a conversation among actors with a common goal. Importantly, it eliminates some basic pitfalls of the dominant shared-memory model, most critically data races. Inquiry: A close look at real-world conversations suggests, however, that they are not mere exchanges of messages. Participants must keep in mind conversational context, and participants joining late can and often must acquire some of this context. In addition, some settings call for engaging in several conversations in parallel; in others, participants conduct temporarily limited sub-conversations to clarify a point. Existing actor code exhibits complex design patterns that get around the underlying limitations of the pure message-passing model. Approach: These patterns suggest a number of elements involved in programming conversational computations. Translated into terms of language design, they call for two kinds of facilities: (1) one for sharing conversational context and (2) another one for organizing individual actors around on-going conversations and their contexts. Knowledge: This paper presents Syndicate, a language designed to directly support the programming of conversing actors. Beyond message passing, it supplies (1) a dataspace, which allows actors to make public assertions, to withdraw them, and to query what other actors have asserted; and (2) the facet notation, which enables programmers to express individual actors as a reflection of the on-going conversations. Grounding: A worked example introduces these concepts and illustrates conversational programming in Syndicate. A comparison with other research and industrial concurrent languages demonstrates the unique support Syndicate provides. Importance: Syndicate advances concurrent actor programming with enhancements that address some observed limitations of the underlying model. While message-passing simplifies concurrent programming, it falls short in handling the complexities of actual computational conversations. By introducing a dataspace actor for sharing conversational context and the facet notation for organizing actors around ongoing conversations, Syndicate enables developers to naturally express and manage the nuanced interactions often required in concurrent systems. These innovations reduce the need for complex design patterns and provide unique support for building robust, context-aware concurrent applications. 2025-02-27T21:40:47Z The Art, Science, and Engineering of Programming, 2025, Vol. 10, Issue 1, Article 2 Sam Caldwell Northeastern University, USA Tony Garnock-Jones Maastricht University, Netherlands Matthias Felleisen Northeastern University, USA 10.22152/programming-journal.org/2026/10/2 http://arxiv.org/abs/2502.20540v1 Study of the Use of Property Probes in an Educational Setting 2025-02-27T21:40:10Z Context: Developing compilers and static analysis tools ("language tools") is a difficult and time-consuming task. We have previously presented *property probes*, a technique to help the language tool developer build understanding of their tool. A probe presents a live view into the internals of the compiler, enabling the developer to see all the intermediate steps of a compilation or analysis rather than just the final output. This technique has been realized in a tool called CodeProber. Inquiry: CodeProber has been in active use in both research and education for over two years, but its practical use has not been well studied. CodeProber combines liveness, AST exploration and presenting program analysis results on top of source code. While there are other tools that specifically target language tool developers, we are not aware of any that has the same design as CodeProber, much less any such tool with an extensive user study. We therefore claim there is a lack of knowledge how property probes (and by extension CodeProber) are used in practice. Approach: We present the results from a mixed-method study of use of CodeProber in an educational setting, with the goal to discover if and how property probes help, and how they compare to more traditional techniques such as test cases and print debugging. In the study, we analyzed data from 11 in-person interviews with students using CodeProber as part of a course on program analysis. We also analyzed CodeProber event logs from 24 students in the same course, and 51 anonymized survey responses across two courses where CodeProber was used. Knowledge: Our findings show that the students find CodeProber to be useful, and they make continuous use of it during the course labs. We further find that the students in our study seem to partially or fully use CodeProber instead of other development tools and techniques, e.g. breakpoint/step-debugging, test cases and print debugging. Grounding: Our claims are supported by three different data sources: 11 in-person interviews, log analysis from 24 students, and surveys with 51 responses. Importance: We hope our findings inspire others to consider live exploration to help language tool developers build understanding of their tool. 2025-02-27T21:40:10Z The Art, Science, and Engineering of Programming, 2025, Vol. 10, Issue 1, Article 10 Anton Risberg Alaküla Lund University, Sweden Niklas Fors Lund University, Sweden Emma Söderberg Lund University, Sweden 10.22152/programming-journal.org/2026/10/10 http://arxiv.org/abs/2502.20538v1 Skitter: A Distributed Stream Processing Framework with Pluggable Distribution Strategies 2025-02-27T21:39:21Z Context: Distributed Stream Processing Frameworks (DSPFs) are popular tools for expressing real-time Big Data applications that have to handle enormous volumes of data in real time. These frameworks distribute their applications over a cluster in order to scale horizontally along with the amount of incoming data. Inquiry: Crucial for the performance of such applications is the **distribution strategy** that is used to partition data and computations over the cluster nodes. In some DSPFs, like Apache Spark or Flink, the distribution strategy is hardwired into the framework which can lead to inefficient applications. The other end of the spectrum is offered by Apache Storm, which offers a low-level model wherein programmers can implement their own distribution strategies on a per-application basis to improve efficiency. However, this model conflates distribution and data processing logic, making it difficult to modify either. As a consequence, today's cluster application developers either have to accept the built-in distribution strategies of a high-level framework or accept the complexity of expressing a distribution strategy in Storm's low-level model. Approach: We propose a novel programming model wherein data processing operations and their distribution strategies are decoupled from one another and where new strategies can be created in a modular fashion. Knowledge: The introduced language abstractions cleanly separate the data processing and distribution logic of a stream processing application. This enables the expression of stream processing applications in a high-level framework while still retaining the flexibility offered by Storm's low-level model. Grounding: We implement our programming model as a domain-specific language, called Skitter, and use it to evaluate our approach. Our evaluation shows that Skitter enables the implementation of existing distribution strategies from the state of the art in a modular fashion. Our performance evaluation shows that the strategies implemented in Skitter exhibit the expected performance characteristics and that applications written in Skitter obtain throughput rates in the same order of magnitude as Storm. Importance: Our work enables developers to select the most performant distribution strategy for each operation in their application, while still retaining the programming model offered by high-level frameworks. 2025-02-27T21:39:21Z The Art, Science, and Engineering of Programming, 2025, Vol. 10, Issue 1, Article 4 Mathijs Saey Vrije Universiteit Brussel, Belgium Joeri De Koster Vrije Universiteit Brussel, Belgium Wolfgang De Meuter Vrije Universiteit Brussel, Belgium 10.22152/programming-journal.org/2026/10/4 http://arxiv.org/abs/2502.20537v1 PolyDebug: A Framework for Polyglot Debugging 2025-02-27T21:39:05Z As software grows increasingly complex, the quantity and diversity of concerns to be addressed also rises. To answer this diversity of concerns, developers may end up using multiple programming languages in a single software project, a practice known as polyglot programming. This practice has gained momentum with the rise of execution platforms capable of supporting polyglot systems. However, despite this momentum, there is a notable lack of development tooling support for developers working on polyglot programs, such as in debugging facilities. Not all polyglot execution platforms provide debugging capabilities, and for those that do, implementing support for new languages can be costly. This paper addresses this gap by introducing a novel debugger framework that is language-agnostic yet leverages existing language-specific debuggers. The proposed framework is dynamically extensible to accommodate the evolving combination of languages used in polyglot software development. It utilizes the Debug Adapter Protocol (DAP) to integrate and coordinate existing debuggers within a debugging session. We found that using our approach, we were able to implement polyglot debugging support for three different languages with little development effort. We also found that our debugger did not introduce an overhead significant enough to hinder debugging tasks in many scenarios; however performance did deteriorate with the amount of polyglot calls, making the approach not suitable for every polyglot program structure. The effectiveness of this approach is demonstrated through the development of a prototype, PolyDebug, and its application to use cases involving C, JavaScript, and Python. We evaluated PolyDebug on a dataset of traditional benchmark programs, modified to fit our criteria of polyglot programs. We also assessed the development effort by measuring the source lines of code (SLOC) for the prototype as a whole as well as its components. Debugging is a fundamental part of developing and maintaining software. Lack of debug tools can lead to difficulty in locating software bugs and slow down the development process. We believe this work is relevant to help provide developers proper debugging support regardless of the runtime environment. 2025-02-27T21:39:05Z The Art, Science, and Engineering of Programming, 2025, Vol. 10, Issue 1, Article 13 Philémon Houdaille University of Rennes, France / CNRS, France / Inria, France Djamel Eddine Khelladi CNRS, France / University of Rennes, France Benoit Combemale University of Rennes, France Gunter Mussbacher McGill University, Canada / Inria, France Tijs van der Storm CWI, Netherlands / University of Groningen, Netherlands 10.22152/programming-journal.org/2026/10/13 http://arxiv.org/abs/2502.20536v1 Automated Profile-Guided Replacement of Data Structures to Reduce Memory Allocation 2025-02-27T21:38:48Z Data structures are a cornerstone of most modern programming languages. Whether they are provided via separate libraries, built into the language specification, or as part of the language's standard library -- data structures such as lists, maps, sets, or arrays provide programmers with a large repertoire of tools to deal with data. Moreover, each kind of data structure typically comes with a variety of implementations that focus on scalability, memory efficiency, performance, thread-safety, or similar aspects. Choosing the *right* data structure for a particular use case can be difficult or even impossible if the data structure is part of a framework over which the user has no control. It typically requires in-depth knowledge about the program and, in particular, about the usage of the data structure in question. However, it is usually not feasible for developers to obtain such information about programs in advance. Hence, it makes sense to look for a more automated way for optimizing data structures. We present an approach to automatically replace data structures in Java applications. We use profiling to determine allocation-site-specific metrics about data structures and their usages, and then automatically replace their allocations with customized versions, focusing on memory efficiency. Our approach is integrated into GraalVM Native Image, an Ahead-of-Time compiler for Java applications. By analyzing the generated data structure profiles, we show how standard benchmarks and microservice-based applications use data structures and demonstrate the impact of customized data structures on the memory usage of applications. We conducted an evaluation on standard and microservice-based benchmarks, in which the memory usage was reduced by up to 13.85 % in benchmarks that make heavy use of data structures. While others are only slightly affected, we could still reduce the average memory usage by 1.63 % in standard benchmarks and by 2.94 % in microservice-based benchmarks. We argue that our work demonstrates that choosing appropriate data structures can reduce the memory usage of applications. While acknowledge that our approach does not provide benefits for all kinds of workloads, our work nevertheless shows how automated profiling and replacement can be used to optimize data structures in general. Hence, we argue that our work could pave the way for future optimizations of data structures. 2025-02-27T21:38:48Z The Art, Science, and Engineering of Programming, 2025, Vol. 10, Issue 1, Article 3 Lukas Makor JKU Linz, Austria Sebastian Kloibhofer JKU Linz, Austria Peter Hofer Oracle Labs, Austria David Leopoldseder Oracle Labs, Austria Hanspeter Mössenböck JKU Linz, Austria 10.22152/programming-journal.org/2026/10/3 http://arxiv.org/abs/2502.20535v1 Probing the Design Space: Parallel Versions for Exploratory Programming 2025-02-27T21:38:23Z Exploratory programming involves open-ended tasks. To evaluate their progress on these, programmers require frequent feedback and means to tell if the feedback they observe is bringing them in the right direction. Collecting, comparing, and sharing feedback is typically done through ad-hoc means: relying on memory to compare outputs, code comments, or manual screenshots. To approach this issue, we designed Exploriants: an extension to example-based live programming. Exploriants allows programmers to place variation points. It collects outputs captured in probes and presents them in a comparison view that programmers can customize to suit their program domain. We find that the addition of variation points and the comparisons view encourages a structured approach to exploring variations of a program. We demonstrate Exploriants' capabilities and applicability in three case studies on image processing, data processing, and game development. Given Exploriants, exploratory programmers are given a straightforward means to evaluate their progress and do not have to rely on ad-hoc methods that may introduce errors. 2025-02-27T21:38:23Z The Art, Science, and Engineering of Programming, 2025, Vol. 10, Issue 1, Article 5 Tom Beckmann Hasso Plattner Institute, Germany / University of Potsdam, Germany Joana Bergsiek Hasso Plattner Institute, Germany / University of Potsdam, Germany Eva Krebs Hasso Plattner Institute, Germany / University of Potsdam, Germany Toni Mattis Hasso Plattner Institute, Germany / University of Potsdam, Germany Stefan Ramson Hasso Plattner Institute, Germany / University of Potsdam, Germany Martin C. Rinard Massachusetts Institute of Technology, USA Robert Hirschfeld Hasso Plattner Institute, Germany / University of Potsdam, Germany 10.22152/programming-journal.org/2026/10/5 http://arxiv.org/abs/2502.20534v1 Consistent Distributed Reactive Programming with Retroactive Computation 2025-02-27T21:38:04Z Context: Many systems require receiving data from multiple information sources, which act as distributed network devices that asynchronously send the latest data at their own pace to generalize various kinds of devices and connections, known as the Internet of Things (IoT). These systems often perform computations both **reactively** and **retroactively** on information received from the sources for monitoring and analytical purposes, respectively. Inquiry: It is challenging to design a programming language that can describe such systems at a high level of abstraction for two reasons: (1) reactive and retroactive computations in these systems are performed alongside the execution of other application logic; and (2) information sources may be distributed, and data from these sources may arrive late or be lost entirely. Addressing these difficulties is our fundamental problem. Approach: We propose a programming language that supports the following features. First, our language incorporates reactive time-varying values (also known as signals) embedded within an imperative language. Second, it supports multiple information sources that are distributed and represented as signals, meaning they can be declaratively composed to form other time-varying values. Finally, it allows computation over past values collected from information sources and recovery from inconsistency caused by packet loss. To address the aforementioned difficulties, we develop a core calculus for this proposed language. Knowledge: This calculus is a hybrid of reactive/retroactive computations and imperative ones. Because of this hybrid nature, the calculus is inherently complex; however, we have simplified it as much as possible. First, its semantics are modeled as a simple, single-threaded abstraction based on typeless object calculus. Meanwhile, reactive computations that execute in parallel are modeled using a simple process calculus and are integrated with the object calculus, ensuring that the computation results are always serialized. Specifically, we show that time consistency is guaranteed in the calculus; in other words, consistency can be recovered at any checkpoint. Grounding: This work is supported by formally stating and proving theorems regarding time consistency. We also conducted a microbenchmarking experiment to demonstrate that the implemented recovery process is feasible in our assumed application scenarios. Importance: The ensured time consistency provides a rigorous foundation for performing analytics on computation results obtained from distributed information sources, even when these sources experience delays or packet loss. 2025-02-27T21:38:04Z The Art, Science, and Engineering of Programming, 2025, Vol. 10, Issue 1, Article 11 Tetsuo Kamina Oita University, Japan Tomoyuki Aotani Sanyo-Onoda City University, Japan Hidehiko Masuhara Institute of Science Tokyo, Japan 10.22152/programming-journal.org/2026/10/11