Session types express and enforce safe communication in concurrent message-passing systems by statically capturing the interaction protocols between processes in the type. Recent works extend session types with arithmetic refinements, which enable additional fine-grained description of communication, but impose additional annotation burden on the programmer. To alleviate this burden, we propose a type inference algorithm for a session type system with arithmetic refinements. We develop a theory of subtyping for session types, including an algorithm which we prove sound with respect to a semantic definition based on type simulation. We also provide a formal inference algorithm that generates type and arithmetic constraints, which are then solved using the Z3 SMT solver. The algorithm has been implemented on top of the Rast language, and includes 3 key optimizations that make inference feasible and practical. We evaluate the efficacy of our inference engine by evaluating it on 6 challenging benchmarks, ranging from unary and binary natural numbers to linear λ -calculus. We show the performance benefits provided by our optimizations in coercing Z3 into solving the arithmetic constraints in reasonable time.
Synthesizing ranking functions is a common technique for proving the termination of loops. A ranking function must be bounded and decrease by a specified amount with each iteration for all reachable program states. Since the set of reachable states is unknown, loop invariants are used to over-approximate it, requiring the joint synthesis of ranking functions and invariants. Existing approaches either synthesize them independently, encode them into a single monolithic query, or connect them through ad hoc, one-way information flow, leading to inefficient exploration of large search spaces. We present Syndicate, a termination analysis framework based on the novel concept of Bidirectional Decompositional Search (BDS). BDS keeps the ranking function and invariant synthesis decomposed but ensures continuous bi-directional feedback. This mutual guidance enables efficient exploration, significantly increasing the number of programs proven to terminate while reducing runtime compared to baselines without such feedback. Depending on the templates used, Syndicate is both relatively complete and provably efficient, outperforming existing techniques that achieve at most one of these guarantees. Despite its simplicity, Syndicate matches or surpasses state-of-the-art tools in termination proofs and runtime, demonstrating the effectiveness of bi-directional reasoning in termination analysis. Github: https://github.com/uiuc-focal-lab/Syndicate
We propose the integration of staged metaprogramming into a session-typed message passing functional language. We build on a model of contextual modal type theory with multi-level contexts, where contextual values, closing arbitrary terms over a series of variables, may be boxed and transmitted in messages. Once received, one such value may then be unboxed and locally applied before being run. To motivate this integration, we present examples of real-world use cases, for which our system would be suitable, such as servers preparing and shipping code on demand via session typed messages. We present a type system that distinguishes linear (used exactly once) from unrestricted (used an unbounded number of times) resources, and further define a type checker, suitable for a concrete implementation. We show type preservation, a progress result for sequential computations and absence of runtime errors for the concurrent runtime environment, as well as the correctness of the type checker.
This paper presents several efficient decision procedures for trace equivalence of GKAT automata, which make use of on-the-fly symbolic techniques via SAT solvers. To demonstrate applicability of our algorithms, we designed symbolic derivatives for CF-GKAT, a practical system based on GKAT designed to validate control-flow transformations. We implemented the algorithms in Rust and evaluated them on both randomly generated benchmarks and real-world control-flow transformations. Indeed, we observed order-of-magnitude performance improvements against existing implementations for both KAT and CF-GKAT. Notably, our experiments also revealed a bug in Ghidra, an industry-standard decompiler, highlighting the practical viability of these systems.
This paper focuses on effective user diagnostics generated during the deductive verification of probabilistic programs. Our key principle is based on providing slices for (1) error reporting, (2) proof simplification, and (3) preserving successful verification results. By formally defining these different notions on HeyVL, an existing quantitative intermediate verification language (IVL), our concepts (and implementation) can be used to obtain diagnostics for a range of probabilistic programming languages. Slicing for error reporting is a novel notion of error localization for quantitative assertions. We demonstrate slicing-based diagnostics on a variety of proof rules such as quantitative versions of the specification statement and invariant-based loop rules, and formally prove the correctness of specialized error messages and verification hints. We implemented our user diagnostics into the deductive verifier Caesar. Our novel implementation — called Brutus — can search for slices which do or do not verify, corresponding to each of the three diagnostic notions. For error reporting (1), it exploits a binary search-based algorithm that minimizes error-witnessing slices. To solve for slices that verify (2 and 3), we empirically compare different algorithms based on unsatisfiable cores, minimal unsatisfiable subset enumeration, and a direct SMT encoding of the slicing problem. Our empirical evaluation of Brutus on existing and new benchmarks shows that we can find slices that are both small and informative.
In earlier work, we developed a modular approach for automatic complexity analysis of integer programs. However, these integer programs do not allow non-tail recursive calls or subprocedures. In this paper, we consider integer programs with function calls and present a natural extension of our modular complexity analysis approach to the recursive setting based on a new form of ranking functions. Hence, our approach combines already existing powerful techniques on the "imperative" parts of the program and our novel ranking functions on the recursive parts. The strength of this combination is demonstrated by our implementation in the complexity analysis tool KoAT.
Choreographic programming (CP) is a method to implement distributed systems that ensures communication deadlock freedom by design. To use CP, though, the number of processes and the network among them must be known statically. Often, that information is known only dynamically. Thus, existing CP languages cannot be used to implement process-parametric distributed systems. This paper introduces first-person choreographic programming (1CP) to support the implementation of process-parametric distributed systems while also ensuring communication deadlock freedom. We present both a design of 1CP (new calculus, formalised in Isabelle/HOL) and an implementation (new language and tooling, integrated in VS Code).
Recurrence relations are used in a wide variety of static program analysis tasks such as loop summarization, invariant generation, and, most classically, modeling the (asymptotic) worst-case runtime behavior of recursive divide-and-conquer algorithms. In this work, we focus on the latter use-case. Classical methods for this problem, such as the well-known Master Theorem (MT) or the Akra-Bazzi method (AB) can only handle single recurrences of a certain limited form. Specifically, MT requires that each instance be divided into a fixed number of smaller sub-instances of the same size. AB generalizes MT by allowing sub-instances of different sizes, but still requires that the number of such sub-instances be fixed and independent of the size of the original instance. Moreover, these methods can handle neither multi-variate recurrences nor systems of recurrences that model non-simple recursive behavior among two or more procedures. In this work, we lift these restrictions and consider a wide family of recurrences called Generalized Polynomial Recurrence Systems (GPRS). Our setting is highly expressive and allows systems of multi-variate recurrences in which an instance can be divided into polynomially-many sub-instances. Moreover, the division is not limited to a single rule and can have several cases based on conditions on the values of the variables. We show how to obtain polynomial upper-bounds for a GPRS using template-based methods and classical theorems from polyhedral and algebraic geometry. Our approach reduces the synthesis of polynomial upper-bounds to linear or semi-definite programming instances, enabling efficient solutions. Crucially, our method is sound and semi-complete, i.e. complete for polynomials of any fixed degree and obtains concrete, as opposed to asymptotic, upper-bounds.
Practical SQL engines differ in subtle ways in their handling of typing constraints and implicit type casts. These issues, usually not considered in formal accounts of SQL, directly affect the portability of queries between engines. To understand this problem, we present a formal typing semantics for SQL, named , that explicitly captures both static and dynamic type behavior. The system is expressed in terms of abstract operators that provide the necessary leeway to precisely model different SQL engines (PostgreSQL, MS SQL Server, MySQL, SQLite, and Oracle). We show that this formalism provides formal guarantees regarding the handling of types. We provide practical conditions on engines to prove type safety and soundness of queries. In this regard, can serve as precise documentation of typing in existing engines and potentially guide their evolution, as well as provide a formal basis to study type-aware query optimizations, and design provably-correct query translators. Additionally, we test the adequacy of the formalism, implementing in Python for these five engines, and tested them with thousands of randomly-generated queries.
We study the relationship between two approaches to higher-order program verification: a semi-automated method using Dijkstra monads and a fully automated method using a higher-order fixpoint logic called HFL(Z). Although the origins of both approaches are quite different, there are some striking similarities: both convert programs to corresponding predicate transformers, and the conversion is essentially obtained by a CPS transformation. After reviewing the two approaches, we formalize an exact correspondence between the two for a restricted fragment of a functional language. We also point out that, outside the restricted fragment, there are some important differences between the two approaches, suggesting the need for cross-fertilization to obtain the best of the two approaches. As an example of the cross-fertilization, we also propose a semi-automated verification method, which requires less annotations than the Dijkstra monad approach and can scale to larger programs than the HFL(Z) approach.
Concurrent randomized programs in the oblivious adversary model are extremely difficult for modular verification because the interaction between threads is very sensitive to the program structure and the execution steps. We propose a new program logic supporting thread-local verification. With a novel “split” mechanism, one can split the state distribution into smaller partitions, and the reasoning can be done based on each partition independently, which allows us to avoid considering different execution paths of branch statements simultaneously. The logic rules are compositional and are natural extensions of their sequential counterparts. Using our program logic, we verify four typical algorithms in the oblivious adversary model.
By decoupling and decomposing control flows, demand control-flow analysis (CFA) resolves only the flow segments determined necessary to produce a specified control-flow fact. It therefore presents a more flexible interface and pricing model than typical CFA, making many useful applications practical. At present, the only realization of demand CFA is the context-insensitive Demand 0CFA. Typical mechanisms for adding context sensitivity are not compatible with the demand setting because the analyzer is dispatched at arbitrary program points in indeterminate contexts. We overcome this challenge by identifying a context suitable for a demand analysis and designing a representation thereof that allows it to model incomplete knowledge of the context. On top of this design, we construct Demand m-CFA, a context-sensitive demand CFA hierarchy. With the attractive pricing model of demand analysis and the precision offered by context sensitivity, we show that Demand m-CFA can replace its exhaustive counterpart in compiler backends and integrate into interactive tools such as language servers.
Remote Direct Memory Access (RDMA) is a modern technology enabling high-performance inter-node communication. Despite its widespread adoption, theoretical understanding of permissible behaviours remains limited, as RDMA follows a very weak memory model. This paper addresses the challenge of establishing sufficient conditions for RDMA robustness. We introduce a set of straightforward criteria that, when met, guarantee sequential consistency and mitigate potential issues arising from weak memory behaviours in RDMA applications. Notably, when restricted to a tree topology, these conditions become even more relaxed, significantly reducing the need for synchronisation primitives. This work provides developers with practical guidelines to ensure the reliability and correctness of their RDMA-based systems.
We introduce coma, a formally defined intermediate verification language. Specification annotations in coma take the form of assertions mixed with the executable program code. A special programming construct representing the abstraction barrier is used to separate, inside a subroutine, the “interface” part of the code, which is verified at every call site, from the “implementation” part, which is verified only once, at the definition site. In comparison with traditional contract-based specification, this offers us an additional degree of freedom, as we can provide separate specification (or none at all) for different execution paths. We define a verification condition generator for coma and prove its correctness. For programs where specification is given in a traditional way, with abstraction barriers at the function entries and exits, our verification conditions are similar to the ones produced by a classical weakest-precondition calculus. For programs where abstraction barriers are placed in the middle of a function definition, the user-written specification is seamlessly completed with the verification conditions generated for the exposed part of the code. In addition, our procedure can factorize selected subgoals on the fly, which leads to more compact verification conditions. We illustrate the use of coma on two non-trivial examples, which have been formalized and verified using our implementation: a second-order regular expression engine and a sorting algorithm written in unstructured assembly code.
We report our experience in enhancing automated grading in an undergraduate programming course using formal verification. In our experiment, we deploy a program verifier to check the equivalence between student submissions and our reference solutions, alongside the existing testing-based grading infrastructure. We were able to use program equivalence to differentiate student submissions according to their high-level program structure, in particular their recursion pattern, even when their input-output behaviour is identical. Consequently, we achieve (1) higher confidence in correctness of idiomatic solutions but also (2) more thorough assessment of solution landscape that reveals solutions beyond those envisioned by instructors.
Algorithmic versions of the Lovász Local Lemma (ALLLs), or rather, the Moser-Tardos algorithm and its variants, are impactful in both theory and practice. In this paper, we take the first step towards the goal of formally verifying ALLLs by applying programming language techniques. We propose two proof recipes, called loop truncation and resampling-table-based coupling, for bridging the gap between Hoare-style program logics and ALLLs’ original informal proofs. We formally verify six existing important results related to ALLLs, and propose a new result which generalizes several existing results. Our proof recipes can also be used to verify general properties of other probabilistic programs in addition to ALLLs.
This artifact report is a companion to the ESOP’25 paper An abstract, certified account of operational game semantics [3]. The paper describes the construction of a sound model for an abstract notion of language. The model is built using a semantic technique named Operational Game Semantics (OGS). All our results are mechanised in the Coq proof assistant: this mechanisation (The proof artifact is archived at https://doi.org/10.5281/zenodo.14697618 .) constitutes the artifact we discuss in the present document. More specifically, our mechanisation covers our main result, the soundness of the abstract OGS model w.r.t. substitution equivalence (Theorem 8), as well as four example calculi: two variants of call-by-value λ -calculus and two variants of μμ̃ -calculus [4, 5]. The only axiom used is the Axiom K [17] for equality proof irrelevance (To ease dependent pattern matching due to the intrinsically scoped representation.). The README explains the installation process and the structure of the code. An online rendering ( https://lapin0t.github.io/ogs/esop25/Readme.html .) is available thanks to Alectryon [12]. Furthermore, the main paper provides systematic hyperlinks from statements to their Coq counterparts. We encourage the interested reader to use these tools to navigate the code. In this document, we focus first on users: how to read and instantiate our main result. We then detail salient technical aspects of our mechanisation.
Named and optional arguments are prevalent features in many mainstream programming languages, enhancing code readability and flexibility. Despite widespread use, their formalization has not been extensively studied. This paper bridges this gap by presenting a type-safe foundation for named and optional arguments using intersection and union types. We begin by identifying a critical type-safety issue in popular static type checkers for Python and Ruby, particularly in handling first-class named arguments in the presence of subtyping. Our solution involves rewriting call sites to ensure type safety, which we formalize through a translation into a core calculus called λ _ . The type safety of the translation is proven using the Coq proof assistant. The practical implementation of our approach in the CP language validates our theoretical contributions. Furthermore, we informally discuss how our approach could be adapted to encode named and optional arguments in other existing languages.
Guarded Interaction Trees are a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Coq. We present an extension of Guarded Interaction Trees to support formal reasoning about context-dependent effects. That is, effects whose behaviors depend on the evaluation context, e.g., call/cc, shift and reset. Using and reasoning about such effects is challenging since certain compositionality principles no longer hold in the presence of such effects. For example, the so-called “bind rule” in modern program logics (which allows one to reason modularly about a term inside a context) is no longer valid. The goal of our extension is to support representation and reasoning about context-dependent effects in the most painless way possible. To that end, our extension is conservative: the reasoning principles (and the Coq implementation) for context-independent effects remain the same. We show that our implementation of context-dependent effects is viable and powerful. We use it to give direct-style denotational semantics for higher-order programming languages with call/cc and with delimited continuations. We extend the program logic for Guarded Interaction Trees to account for context-dependent effects, and we use the program logic to prove that the denotational semantics is adequate with respect to the operational semantics. This is achieved by constructing logical relations between syntax and semantics inside the program logic. Additionally, we retain the ability to combine multiple effects in a modular way, which we demonstrate by showing type soundness for safe interoperability of a programming language with delimited continuations and a programming language with higher-order store.
