Programming Languages and Systems

Existing Curry-Howard interpretations of call-by-value evaluation for the \(\lambda \)-calculus are either based on ad-hoc modifications of intuitionistic proof systems or involve additional logical concepts such as classical logic or linear logic, despite the fact that call-by-value was introduced in an intuitionistic setting without linear features.

We introduce a novel approach to studying properties of processes in the \(\pi \)-calculus based on a processes-as-formulas interpretation, by establishing a correspondence between specific sequent calculus derivations and computation trees in the reduction semantics of the recursion-free \(\pi \)-calculus. Our method provides a simple logical characterisation of deadlock-freedom for the recursion- and race-free fragment of the \(\pi \)-calculus, supporting key features such as cyclic dependencies and an independence of the name restriction and parallel operators. Based on this technique, we establish a strong completeness result for a nontrivial choreographic language: all deadlock-free and race-free finite \(\pi \)-calculus processes composed in parallel at the top level can be faithfully represented by a choreography.

With these results, we show how the computation-as-derivation paradigm extends the reach of logical methods for the study of concurrency, by bridging gaps between logic, the expressiveness of the \(\pi \)-calculus, and the expressiveness of choreographic languages.

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.

De Nicola and Hennessy’s \(\textsc {must}\)-preorder is a liveness preserving refinement which states that a server \(q\) refines a server \(p\) if all clients satisfied by \(p\) are also satisfied by \(q\). Owing to the universal quantification over clients, this definition does not yield a practical proof method, and alternative characterisations are necessary to reason over it. Finding these characterisations for asynchronous semantics, i.e. where outputs are non-blocking, has thus far proven to be a challenge, usually tackled via ad-hoc definitions.

We show that the standard characterisations of the \(\textsc {must}\)-preorder carry over as they stand to asynchronous communication, if servers are enhanced to act as forwarders, i.e. they can input any message as long as they store it back into the shared buffer. Our development is constructive, is completely mechanised in Coq, and is independent of any calculus: our results pertain to Selinger output-buffered agents with feedback. This is a class of Labelled Transition Systems that captures programs that communicate via a shared unordered buffer, as in asynchronous CCS or the asynchronous \(\pi \)-calculus.

We show that the standard coinductive characterisation lets us prove in Coq that concrete programs are related by the \(\textsc {must}\)-preorder.

Finally, our proofs show that Brouwer’s bar induction principle is a useful technique to reason on liveness preserving program transformations.

We introduce a new abstract domain for analyzing memory block manipulations, focusing on programs with dynamically allocated arrays. This domain computes properties universally quantified over the value of the loop counters, both for assignments and tests. These properties consist of equalities and comparison predicates involving abstract expressions, represented as affine forms in the loop counters and symbolic dereferences. All these methods have been incorporated within the Astrée© static analyzer that checks for the absence of run-time errors in embedded critical software. We also give insights on how to implement this abstract domain within any other C static analyzer.

Charts, figures, and text derived from data play an important role in decision making. But making sense of or fact-checking outputs means understanding how they relate to the underlying data. Even for experts with access to the source code and data sets, this poses a significant challenge. We introduce a new program analysis framework (A supporting artifact is available at https://​zenodo.​org/​records/​14637654 [5].) which supports interactive exploration of fine-grained IO relationships directly through computed outputs, using dynamic dependence graphs. This framework enables a novel notion in data provenance which we call linked inputs, a relation of mutual relevance or cognacy which arises between inputs that contribute to common features of the output. We give a procedure for computing linked inputs over a dependence graph, and show how the presented in this paper is faster on most examples than an implementation based on execution traces.

Operational game semantics (OGS) is a method for interpreting programs as strategies in suitable games, or more precisely as labelled transition systems over suitable games, in the sense of Levy and Staton. Such an interpretation is called sound when, for any two given programs, weak bisimilarity of associated strategies entails contextual equivalence. OGS has been applied to a variety of languages, with rather tedious soundness proofs.

In this paper, we contribute to the unification and mechanisation of OGS. Indeed, we propose an abstract notion of language with evaluator, for which we construct a generic OGS interpretation, which we prove sound. Our framework covers a variety of simply-typed and untyped lambda-calculi with various evaluation strategies. These calculi notably feature recursive definitions, first-class continuations, and a wide variety of datatypes. All constructions and proofs are entirely mechanised in the Coq proof assistant.

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 \(\lambda \)-calculus and two variants of \(\mu \tilde{\mu }\)-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.

Neural network verification is a new and rapidly developing field of research. So far, the main priority has been establishing efficient verification algorithms and tools, while proper support from the programming language perspective has been considered secondary or unimportant. Yet, there is mounting evidence that insights from the programming language community may make a difference in the future development of this domain. In this paper, we formulate neural network verification challenges as programming language challenges and suggest possible future solutions.

A hierarchy of type universes is a rudimentary ingredient in the type theories of many proof assistants to prevent the logical inconsistency resulting from combining dependent functions and the type-in-type axiom. In this work, we argue that a universe hierarchy is not the only option for universes in type theory. Taking inspiration from Leivant’s Stratified System F, we introduce Stratified Type Theory (StraTT), where rather than stratifying universes by levels, we stratify typing judgements and restrict the domain of dependent functions to strictly lower levels. Even with type-in-type, this restriction suffices to enforce consistency.

In StraTT, we consider a number of extensions beyond just stratified dependent functions. First, the subsystem subStraTT employs McBride’s crude-but-effective stratification (also known as displacement) as a simple form of level polymorphism where global definitions with concrete levels can be displaced uniformly to any higher level. Second, to recover some expressivity lost due to the restriction on dependent function domains, the full StraTT includes a separate nondependent function type with a floating domain whose level matches that of the overall function type. Finally, we have implemented a prototype type checker for StraTT extended with datatypes and inference for level and displacement annotations, along with a small core library.

We have proven subStraTT to be consistent and StraTT to be type safe, but consistency of the full StraTT remains an open problem, largely due to the interaction between floating functions and cumulativity of judgements. Nevertheless, we believe StraTT to be consistent, and as evidence have verified the ill-typedness of some well-known type-theoretic paradoxes using our implementation.

Dependent pattern matching is a key feature in dependently typed programming. However, there is a theory-practice disconnect: while many proof assistants implement pattern matching as primitive, theoretical presentations give semantics to pattern matching by elaborating to eliminators. Though theoretically convenient, eliminators can be awkward and verbose, particularly for complex combinations of patterns.

This work aims to bridge the theory-practice gap by presenting a direct categorical semantics for pattern matching, which does not elaborate to eliminators. This is achieved using sheaf theory to describe when sets of arrows (terms) can be amalgamated into a single arrow. We present a language with top-level dependent pattern matching, without specifying which sets of patterns are considered covering for a match. Then, we give a sufficient criterion for which pattern-sets admit a sound model: patterns should be in the canonical coverage for the category of contexts. Finally, we use sheaf-theoretic saturation conditions to devise some allowable sets of patterns. We are able to express and exceed the status quo, giving semantics for datatype constructors, nested patterns, absurd patterns, propositional equality, and dot patterns.

Variable Elimination (\(\textsf{VE}\)) is a classical exact inference algorithm for probabilistic graphical models such as Bayesian Networks, computing the marginal distribution of a subset of the random variables in the model. Our goal is to understand Variable Elimination as an algorithm acting on programs in an idealized probabilistic functional language—a linear simply-typed \(\lambda \)-calculus suffices for our purpose. Precisely, we express \(\textsf{VE}\) as a term rewriting process, which transforms a global definition of a variable into a local definition, by swapping and nesting let-in expressions. We exploit in an essential way linear types.

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.

In this paper, we overcome these limitations by providing an iso-recursive typing system that computes the behavioural properties of environments. The type system relies on a terminating function named compliance that computes all final redexes of an environment, and determines when these redexes do not contain mismatches or deadlocks: compliant environments cannot go wrong. The function is defined theoretically by introducing the novel notions of deterministic LTS of environments and of environment closure, and can be implemented in mainstream programming languages and compilers. We showcase an implementation in OCaml by using exception handling to tackle the inherent non-determinism of synchronisation of branching and selection types. We assess that the implementation provides the desired properties, namely absence of mismatches and of deadlocks in environments, by resorting to automated deductive verification performed in tools of the OCaml ecosystem relying on Why3.

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.

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 \(\textsf{TRAF} \), that explicitly captures both static and dynamic type behavior. The system \(\textsf{TRAF} \) 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, \(\textsf{TRAF} \) 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 \(\textsf{TRAF} \) in Python for these five engines, and tested them with thousands of randomly-generated queries.