Programming Languages and Systems

Inhaltsverzeichnis

1. Frontmatter

2. Type Systems, Safety, and Verification

   1. Frontmatter

   2. Memory Safety: Uniqueness as Separation

      Pilar Selene Linares Arévalo, Arthur Azevedo de Amorim, Vincent Jackson, Liam O’Connor, Peter Schachte, Christine Rizkallah

      Abstract

      Programming languages with uniqueness type systems prevent pointer aliasing, simplifying memory safety reasoning. However, code implemented in these languages often interoperates through foreign function interfaces with external components implemented in languages lacking the same level of static safety guarantees. To verify safe updates in a combined system, one must manually verify that the external components preserve the safety invariants of the uniqueness type system. In particular, recent work showed that one can manually discharge such obligations on C components from a cross-language Cogent-C system by directly reasoning about the C code in higher-order logic. However, even for simple examples, discharging the uniqueness safety obligations, known as frame conditions, within a logic not specifically designed for direct reasoning in terms of heaps and pointers was not ideal. Separation logic is an established logic that facilitates reasoning about imperative programs by localising reasoning to the parts of the heap that the program mutates. This raises a vital question. Can we use separation logic to discharge the safety obligations imposed by uniqueness types? The answer is yes. This paper demonstrates that the frame conditions can be inferred from particular separation logic triples and, hence, discharged by reasoning using separation logic. We identify and verify the soundness of specific separation logic triples that imply the frame conditions imposed by a uniqueness type system.

   3. Fair Termination for Resource-Aware Active Objects

      Francesco Dagnino, Paola Giannini, Violet Ka I Pun, Ulises Torrella

      Abstract

      Active object systems are a model of distributed computation that has been adopted for modelling distributed systems and business process workflows. This field of modelling is, in essence, concurrent and resource-aware, motivating the development of resource-aware formalisations on the active object model. The contributions of this work are the development of a core calculus for resource-aware active objects together with a type system ensuring that well-typed programs are fairly terminating, i.e., they can always eventually terminate. To achieve this, we combine techniques from graded semantics and type systems, which are quite well understood for sequential programs, with those for fair termination, which have been developed for synchronous sessions.

   4. A Formal Foundation for Equational Reasoning on Probabilistic Programs

      Reynald Affeldt, Yoshihiro Ishiguro, Zachary Stone

      Abstract

      Probabilistic programs with sampling and scoring are used to write probabilistic models to make probabilistic inferences. Despite their effectful nature, such programs can actually be verified by means of equational reasoning. We propose a formal foundation in the Rocq prover to mechanize such verifications. For that purpose, we extend an existing library for Lebesgue integration and formalize standard probability distributions. Using the resulting library, we extend the intrinsically-typed syntax and the kernel-based semantics of an encoding of a probabilistic programming language. Thanks to these extensions, we mechanize the main running examples of Shan’s tutorial on equational reasoning for probabilistic programming at POPL 2018’s TutorialFest.

3. Control, Effects, and Decidability

   1. Frontmatter

   2. Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers

      Ryunosuke Endo, Tachio Terauchi

      Abstract

      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.

   3. Expressive Power of One-Shot Control Operators and Coroutines

      Kentaro Kobayashi, Yukiyoshi Kameyama

      Abstract

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

   4. Positive Sharing and Abstract Machines

      Beniamino Accattoli, Claudio Sacerdoti Coen, Jui-Hsuan Wu

      Abstract

      Wu’s positive \(\lambda \)-calculus is a recent call-by-value \(\lambda \)-calculus with sharing coming from Miller and Wu’s study of the proof-theoretical concept of focalization. Accattoli and Wu showed that it simplifies a technical aspect of the study of sharing; namely it rules out the recurrent issue of renaming chains, that often causes a quadratic time slowdown.

      In this paper, we define the natural abstract machine for the positive \(\lambda \)-calculus and show that it suffers from an inefficiency: the quadratic slowdown somehow reappears when analyzing the cost of the machine. We then design an optimized machine for the positive \(\lambda \)-calculus, which we prove efficient. The optimization is based on a new slicing technique which is dual to the standard structure of machine environments.

4. Quantum Programming and Logic

   1. Frontmatter

   2. IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation

      Kinnari Dave, Alejandro Díaz-Caro, Vladimir Zamdzhiev

      Abstract

      We introduce a proof language for Intuitionistic Multiplicative Additive Linear Logic (IMALL), extended with a modality \(\mathcal B\) to capture mixed-state quantum computation. The language supports algebraic constructs such as linear combinations, and embeds pure quantum computations within a mixed-state framework via \(\mathcal B\), interpreted categorically as a functor from a category of Hilbert Spaces to a category of finite-dimensional C*-algebras. Measurement arises as a definable term, not as a constant, and the system avoids the use of quantum configurations, which are part of the theory of the quantum lambda calculus. Cut-elimination is defined via a composite reduction relation, and shown to be sound with respect to the denotational interpretation. We prove that any linear map on \(\mathbb C^{2^n}\) can be represented within the system, and illustrate this expressiveness with examples such as quantum teleportation and the quantum switch.

   3. A Quantum-Control Lambda-Calculus with Multiple Measurement Bases

      Alejandro Díaz-Caro, Nicolas A. Monzon

      Abstract

      We introduce Lambda-SX, a typed quantum lambda-calculus that supports multiple measurement bases. By tracking duplicability relative to arbitrary bases within the type system, Lambda-SX enables more flexible control and compositional reasoning about measurements. We formalise its syntax, typing rules, subtyping, and operational semantics, and establish its key meta-theoretical properties. This proof-of-concept shows that support for multiple bases can be coherently integrated into the type discipline of quantum programming languages.

5. Program Analysis, Specifications, and Decision Procedures

   1. Frontmatter

   2. Checking Consistency of Event-Driven Traces

      Parosh Aziz Abdulla, Mohamed Faouzi Atig, R. Govind, Samuel Grahn, Ramanathan S. Thinniyam

      Abstract

      Event-driven programming is a popular paradigm where the flow of execution is controlled by two features: (1) shared memory and (2) sending and receiving of messages between multiple handler threads (just called handler). Each handler has a mailbox (modelled as a queue) for receiving messages, with the constraint that the handler processes its messages sequentially. Executions of messages by different handlers may be interleaved. A central problem in this setting is checking whether a candidate execution is consistent with the semantics of event-driven programs. In this paper, we propose an axiomatic semantics for event-driven programs based on the standard notion of traces (also known as execution graphs). We prove the equivalence of axiomatic and operational semantics. This allows us to rephrase the consistency problem axiomatically, resulting in the event-driven consistency problem: checking whether a given trace is consistent. We analyze the computational complexity of this problem and show that it is NP-complete, even when the number of handler threads is bounded. We then identify a tractable fragment: in the absence of nested posting, where handlers do not post new messages while processing a message, consistency checking can be performed in polynomial time. Finally, we implement our approach in a prototype tool and report on experimental results on a wide range of benchmarks.

   3. Specification Inference Modulo Oracles for Database-Backed Web Applications

      Nitesh Trivedi, Subhajit Roy

      Abstract

      In logical reasoning, specification inference attempts to synthesize an explanatory hypothesis from a given conclusion. We consider the specification synthesis problem for database-backed web-applications where only an oracle access to the application is available. Such is a real case for test teams where they are not provided access to the application. Our algorithm begins with an initial hypothesis constructed from responses of the web-application on a sampled dataset, and then improves this hypothesis iteratively via carefully constructed queries to the application (via an SMT solver). Finally, statistical tests are used to validate the soundness and maximality of the constructed hypothesis. We implement our algorithm in a tool, Vivaran, and demonstrate its capabilities on a large web-based enterprise resource planning (ERP) software. Vivaran infers semantically equivalent specifications as the ground-truth in all cases.

   4. Decision Procedure for a Theory of String Sequences

      Denghang Hu, Taolue Chen, Philipp Rümmer, Fu Song, Zhilin Wu

      Abstract

      The theory of sequences, supported by many SMT solvers, can model program data types including bounded arrays and lists. Sequences are parameterized by the element data type and provide operations such as accessing elements, concatenation, forming sub-sequences and updating elements. Strings and sequences are intimately related; many operations, e.g., matching a string according to a regular expression, splitting strings, or joining strings in a sequence, are frequently used in string-manipulating programs. Nevertheless, these operations are typically not directly supported by existing SMT solvers, which instead only consider the generic theory of sequences. In this paper, we propose a theory of string sequences and study its satisfiability. We show that, while it is undecidable in general, the decidability can be recovered by restricting to the straight-line fragment. This is shown by encoding each string sequence as a string, and each string sequence operation as a corresponding string operation. We provide pre-image computation for the resulting string operations with respect to automata, effectively casting it into the generic OSTRICH string constraint solving framework. We implement the new decision procedure as a tool \(\mathsf{OSTRICH^{SEQ}}\), and carry out experiments on benchmark constraints generated from real-world JavaScript programs, hand-crafted templates and unit tests. The experiments confirm the efficacy of our approach.

6. AI and Compiler Optimisation for Performance

   1. Frontmatter

   2. ELTC: An End-to-End Large Language Model-Based Tensor Compilation Optimization Framework

      WenBo Ma, QingZeng Song, Fei Qiao, YongJiang Xue, MingZe Sun

      Abstract

      Tensor program optimization is a non-convex optimization problem, and efficiently solving it while balancing optimization efficiency and execution performance remains a challenging task. Search-based tensor program compilers have proven effective by constructing large-scale exploration spaces that include potentially high-performance program variants, thus overcoming the performance bottlenecks of traditional program optimization methods. However, these approaches still face significant challenges in search strategies, as existing compilers often require hours or even days to identify the optimal program representation. This paper proposes ELTC, an end-to-end tensor program compilation framework based on large language models (LLMs), designed for efficient optimization of tensor programs in deep neural networks. ELTC formulates the tensor program exploration problem as a generation task for language models. By training a large language model offline, it generates transformation sequences for tensor programs in an end-to-end manner based on their feature representations. While preserving the broad search space, this approach significantly improves optimization efficiency. Moreover, we introduce a language-model-friendly intermediate representation, which encodes key features of tensor programs using structured textual formats. Based on this representation, we construct a tensor program dataset tailored for language models. Experimental results demonstrate that ELTC achieves superior performance in both optimization quality and tuning speed. Compared with the fully converged Ansor-TenSet, ELTC achieves a \(34.07\times \) compilation speedup and an average performance improvement of \(1.06\times \) under convergence conditions. Furthermore, ELTC outperforms the manually optimized kernel library TensorRT, achieving a \(1.3\times \) performance gain.

   3. Performance Optimization of HPC Workloads in Cloud Using AI-Driven Algorithms

      Aman Iftekhar, Rahul Mishra

      Abstract

      As High-Performance Computing (HPC) workloads increasingly migrate to cloud infrastructures, the need for intelligent, inference-time adaptive scheduling becomes critical. Conventional schedulers such as FCFS or SJF often struggle to adapt to the heterogeneous and dynamic nature of cloud-based systems, leading to inefficient resource utilization and increased job wait times. This paper proposes a multi-stage AI-based pipeline to address these challenges through the integration of three core capabilities: job runtime prediction using supervised learning, anomaly detection via deep autoencoders, and adaptive resource scheduling using reinforcement learning. Leveraging real-world data from the MIT SuperCloud dataset, our system extracts meaningful patterns from time-series telemetry to support informed scheduling decisions. The job prediction module estimates runtimes based on CPU utilization, memory consumption, and I/O statistics. The anomaly detection module flags abnormal jobs using learned GPU performance norms. The RL scheduler dynamically matches jobs to compute nodes based on predicted duration and anomaly status, optimizing for turnaround time and utilization. Experimental evaluations demonstrate a 28% reduction in average turnaround time and over 10% increase in resource utilization compared to traditional schedulers. These results establish the viability of AI-driven orchestration strategies in HPC cloud platforms and underscore the importance of integrated learning-based systems in achieving scalable, efficient, and context-aware workload management.

7. Backmatter