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.
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
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× compilation speedup and an average performance improvement of 1.06× under convergence conditions. Furthermore, ELTC outperforms the manually optimized kernel library TensorRT, achieving a 1.3× performance gain.
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.
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.
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.
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 𝖮𝖲𝖳𝖱𝖨𝖢𝖧^𝖲𝖤𝖰 , 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.
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.
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.
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 eventdriven 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.
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.
Wu's positive λ-calculus is a recent call-by-value λ-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 λ-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 λ-calculus, which we prove efficient. The optimization is based on a new slicing technique which is dual to the standard structure of machine environments.
We introduce a proof language for Intuitionistic Multiplicative Additive Linear Logic (IMALL), extended with a modality 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 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 n that any linear map on C 2 can be represented within the system, and illustrate this expressiveness with examples such as quantum teleportation and the quantum switch.
A logical approach to automated program verification has been drawing attention recently, where various program verification problems are transformed into formulas of fixpoint logics such as CHC and ν HFL(Z), so that a given program satisfies a property just if the corresponding fixpoint formula is valid. In this paper, we show a kind of converse transformation, converting fixpoint logic formulas to programs so that a formula is valid just if the resulting program never evaluates to an (error) value. This, together with the aforementioned transformation from programs to formulas, allows us to go back and forth between logical formulas and programs. In particular, our transformation enables us to use random testing to disprove a given formula, implying that the original program does not satisfy the specified property. As the programs generated by a naive transformation are not suitable for random testing, we employ mode analysis to generate more test-friendly programs. We have implemented the mode-guided transformation and confirmed its effectiveness through experiments.
Relational logics aim to stablish properties of two expressions by combining synchronous proof rules, which reason about structurally equivalent expressions, with asynchronous proof rules, which only reason about one of the two expressions. As a result, relational logics are not syntax-directed and their algorithmic implementation is challenging. In this work, we design OBRA an algorithmic, relational, and bidirectional type system that only has synchronous rules to preserve predictability and relies on an external oracle to handle syntactic differences. We formalize OBRA and prove that it is equivalent to Relational Higher-Order Logic (RHOL). We implement OBRA by extending Liquid Haskell with synchronous relational rules and using user-provided unary proofs as the external oracle. Further, OBRA automatically translates relational properties to unary theorems with proof templates that can be manually augmented, debugged, and verified using Liquid Haskell. We evaluate OBRA on 12 benchmarks out of which 7 were proved automatically and the rest required smaller or equal proofs than the unary case.
Stateless model checking (SMC) is crucial for productivity in verified concurrent programming, and its recent developments for C/C++ and weak memory models are remarkable. The state-of-the-art SMC for C, GenMC, efficiently verifies C programs based on C11 atomics and pthreads. However, it does not support mixed-size accesses, accesses to the same memory region with different-sized types, even though they are ubiquitous in C/C++, particularly the code for memory management. As a result, GenMC does not work for C/C++ programs containing memory management. To resolve this problem, we develop a method of adapting GenMC to mixed-size accesses preserving its optimality. We experimentally evaluate the efficiency of our extended implementation of GenMC and its efficacy for memory management programs.
We developed SCV, a verification tool geared towards contracts implemented in Michelson, the smart contract language of the Tezos blockchain. SCV utilizes symbolic execution to derive verification conditions that can be checked automatically against user specifications using an SMT solver. These specifications are written in a domain-specific language. We present the fundamental principles behind the design and development of SCV. By pruning states during symbolic execution, SCV effectively addresses the problem of state explosion. This approach has enabled us to conduct two case studies on real-life contracts, demonstrating the expressiveness of our tool.
Algebraic theories with dependency between sorts form the structural core of Martin-Löf type theory and similar systems. Their denotational semantics are typically studied using categorical techniques; many different categorical structures have been introduced to model them (contextual categories, categories with families, display map categories, etc.) Comparisons of these models are scattered throughout the literature, and a detailed, big-picture analysis of their relationships has been lacking. We aim to provide a clear and comprehensive overview of the relationships between as many such models as possible. Specifically, we take comprehension categories as a unifying language, and show how almost all established notions of model embed as sub-2-categories (usually full) of the 2-category of comprehension categories.
Functions containing arithmetic operations have often restrictions not expressible by standard type systems of programming languages. The division operation requires that the divisor is non-zero and the factorial function should not be applied to negative numbers. Such partial operations might lead to program crashes if they are applied to unintended arguments. Checking the arguments before each call is tedious and decreases the run-time efficiency. To avoid these disadvantages and support the safe use of partially defined operations, we present an approach to verify the correct use of operations at compile time. To simplify its use, our approach automatically infers non-fail conditions of operations from their definitions and checks whether these conditions are satisfied for all uses of the operations. Arithmetic conditions can be verified by SMT solvers, whereas conditions in operations defined on algebraic data types can be inferred and verified by appropriate type abstractions. Therefore, we present a hybrid method which is applicable to larger programs since only a few arithmetic non-fail conditions need to be checked by an external SMT solver. This approach is implemented for functional logic Curry programs so that it is also usable for purely functional or logic programs.
Incorrectness Separation Logic (ISL) is a proof system that is tailored specifically to resolve problems of under-approximation in programs that manipulate heaps, and it primarily focuses on bug detection. This approach is different from the over-approximation methods that are used in traditional logics such as Hoare Logic or Separation Logic. Although the soundness of ISL has been established, its completeness remains unproven. In this study, we establish relative completeness by leveraging the expressiveness of the weakest postconditions; expressiveness is a factor that is critical to demonstrating relative completeness in Reverse Hoare Logic. In our ISL framework, we allow for infinite disjunctions in disjunctive normal forms, where each clause comprises finite symbolic heaps with existential quantifiers. To compute the weakest postconditions in ISL, we introduce a canonicalization that includes variable aliasing.
