title: Bialgebraic Reasoning on Stateful Languages

authors:
Sergey Goncharov
Stefan Milius
Lutz Schröder
Stelios Tsampas
Henning Urbat

abstract: Reasoning about program equivalence in imperative languages is notoriously challenging, as the presence of states (in the form of variable stores) fundamentally increases the observational power of program terms. The key desideratum for any notion of equivalence is compositionality, guaranteeing that subprograms can be safely replaced by equivalent subprograms regardless of the context. To facilitate compositionality proofs and avoid boilerplate work, one would hope to employ the abstract bialgebraic methods provided by Turi and Plotkin’s powerful theory of mathematical operational semantics (a.k.a. abstract GSOS) or its recent extension by Goncharov et al. to higher-order languages. However, multiple attempts to apply abstract GSOS to stateful languages have thus failed. We propose a novel approach to the operational semantics of stateful languages based on the formal distinction between readers (terms that expect an initial input store before being executed), and writers (running terms that have already been provided with a store). In contrast to earlier work, this style of semantics is fully compatible with abstract GSOS, and we can thus leverage the existing theory to obtain coinductive reasoning techniques. We demonstrate that our approach generates non-trivial compositionality results for stateful languages with first-order and higher-order store and that it flexibly applies to program equivalences at different levels of granularity, such as trace, cost, and natural equivalence.


venue: icfp

title: Big Steps in Higher-Order Mathematical Operational Semantics

authors:
Sergey Goncharov
Pouya Partow
Stelios Tsampas

abstract: Small-step and big-step operational semantics are two fundamental styles of structural operational semantics (SOS), extensively used in practice. The former one is more fine-grained and is usually regarded as primitive, as it only defines a one-step reduction relation between a given program and its direct descendant under an ambient evaluation strategy. The latter one implements, in a self-contained manner, such a strategy directly by relating a program to the net result of the evaluation process. The agreement between these two styles of semantics is one of the key pillars in operational reasoning on programs; however, such agreement is typically proven from scratch every time on a case-by-case basis. A general, abstract mathematical argument behind this agreement is up till now missing. We cope with this issue within the framework of higher-order mathematical operational semantics by providing an abstract categorical notion of big-step SOS, complementing the existing notion of abstract higher-order GSOS. Moreover, we introduce a general construction for deriving the former from the latter, and prove an abstract equivalence result between the two.


title: A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware

authors:
Liyi Li
David Young
James Bryan Graves
Chandeepa Dissanayake
Amr Sabry

abstract: In physics and chemistry, quantum systems are typically modeled using energy constraints formulated as Hamiltonians. Investigations into such systems often focus on the evolution of the Hamiltonians under various initial conditions, an approach summarized as Adiabatic Quantum Computing (AQC). Although this perspective may initially seem foreign to functional programmers, we demonstrate that conventional functional programming abstractions—specifically, the Traversable and Monad type classes—naturally capture the essence of AQC. To illustrate this connection, we introduce EnQ, a functional programming library designed to express diverse optimization problems as energy constraint computations (ECC). The library comprises three core components: generating the solution space, associating energy costs with potential solutions, and searching for optimal or near-optimal solutions. Because EnQ is implemented using standard Haskell, it can be executed directly through conventional classical Haskell compilers. More interestingly, we develop and implement a process to compile EnQ programs into circuits executable on quantum hardware. We validate EnQ’s effectiveness through a number of case studies, demonstrating its capacity to express and solve classical optimization problems on quantum hardware, including search problems, type inference, number partitioning, clique finding, and graph coloring.


title: 2-Functoriality of Initial Semantics, and Applications

authors:
Benedikt Ahrens
Ambroise Lafont
Thomas Lamiaux

abstract:
Initial semantics aims to model inductive structures and their properties, and to provide them with recursion principles respecting these properties. An ubiquitous example is the fold operator for lists. We are concerned with initial semantics that model languages with variable binding and their substitution structure, and that provide substitution-safe recursion principles.

There are different approaches to implementing languages with variable binding depending on the choice of representation for contexts and free variables, such as unscoped syntax, or well-scoped syntax with finite or infinite contexts. Abstractly, each approach corresponds to choosing a different monoidal category to model contexts and binding, each choice yielding a different notion of "model" for the same abstract specification (or "signature").

In this work, we provide tools to compare and relate the models obtained from a signature for different choices of monoidal category. We do so by showing that initial semantics naturally has a 2-categorical structure when parametrized by the monoidal category modeling contexts. We thus can relate models obtained from different choices of monoidal categories provided the monoidal categories themselves are related.

In particular, we use our results to relate the models of the different implementation - de Bruijn vs locally nameless, finite vs infinite contexts -, and to provide a generalized recursion principle for simply-typed syntax.


title: Frex: Dependently Typed Algebraic Simplification

authors:
Guillaume Allais
Edwin C. Brady
Nathan Corbyn
Ohad Kammar
Jeremy Yallop

abstract: We present a new design for an algebraic simplification library structured around concepts from universal algebra: theories, models, homomorphisms, and universal properties of free algebras and free extensions of algebras. The library's dependently typed interface guarantees that both built-in and user-defined simplification modules are terminating, sound, and complete with respect to a well-specified class of equations. We have implemented the design in the Idris 2 and Agda dependently typed programming languages and shown that it supports modular extension to new theories, proof extraction and certification, goal extraction via reflection, and interactive development.


title: SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F

authors:
Cezar-Constantin Andrici
Danel Ahman
Catalin Hritcu
Ruxandra Icleanu
Guido Martínez
Exequiel Rivas
Théo Winterhalter

abstract: We introduce SecRef*, a secure compilation framework protecting stateful programs verified in F* against linked unverified code, with which the program dynamically shares ML-style mutable references. To ease program verification in this setting, we track which references are shareable with the unverified code, and which ones are not shareable and whose contents are thus guaranteed to be unchanged after calling into unverified code. This universal property of non-shareable references is exposed in the interface on which the verified program can rely when calling into unverified code. The remaining refinement types and pre- and post-conditions that the verified code expects from the unverified code are converted into dynamic checks about the shared references by using higher-order contracts. We prove formally in F* that this strategy ensures sound and secure interoperability with unverified code. Since SecRef* is built on top of the Monotonic State effect of F*, these proofs rely on the first monadic representation for this effect, which is a contribution of our work that can be of independent interest. Finally, we use SecRef* to build a simple cooperative multi-threading scheduler that is verified and that securely interacts with unverified threads.


title: Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language

authors:
Rutger Broekhoff
Robbert Krebbers

abstract:
To study the semantics of a programming language, it is useful to consider different specification forms—e.g., a substitution-based small-step operational semantics and an environment-based interpreter—because they have mutually exclusive benefits. Developing these specifications and proving correspondences is challenging for ‘dynamic’/‘scripting’ languages such as JavaScript, PHP and Bash. We study this challenge in the context of the Nix expression language, a dynamic language used in the eponymous package manager and operating system. Nix is a Turing-complete, untyped functional language designed for the manipulation of JSON-style attribute sets, with tricky features such as overloaded use of variables for lambda bindings and attribute members, subtle shadowing rules, a mixture of evaluation strategies, and tricky mechanisms for recursion.

We show that our techniques are applicable beyond Nix by starting from the call-by-name lambda calculus, which we extend to a core lambda calculus with dynamically computed variable names and dynamic binder names, and finally to Nix. Our key novelty is the use of a form of deferred substitutions, which enables us to give a concise substitution-based semantics for dynamic variable binding. We develop corresponding environment-based interpreters, which we prove to be sound and complete (for terminating, faulty and diverging programs) w.r.t. our operational semantics based on deferred substitutions.

We mechanize all our results in the Rocq prover and showcase a new feature of the Rocq-std++ library for representing syntax with maps in recursive positions. We use Rocq’s extraction mechanism to turn our Nix interpreter into executable OCaml code, which we apply to the official Nix language tests. Altogether this gives rise to the most comprehensive formal semantics for the Nix expression language to date.


title: Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages

authors:
J. A. Carr
Benjamin Quiring
John H. Reppy
Olin Shivers
Skye Soss
Byron Zhong

abstract:
The representation of functions in higher-order languages includes both the function’s code and an environment structure that captures the bindings of the function’s free variables. This paper explores caller-provided environments, where instead of packaging the entirety of a function’s environment in its closure, a function can be provided with a portion of its environment by its caller. In higher-order languages, it is difficult to determine where functions are called, let alone what pieces of the function’s environment are available to be provided by the caller, thus we need a higher-order control-flow analysis to enable caller-provided environments.

In this paper, we present a new abstract-interpretation-based analysis that discovers which pieces of a function’s environment are always shared between its definition and its callers. In such cases, the caller can provide the environment to the callee. Our analysis has been formalized in the Rocq proof assistant. We evaluate our analysis on a collection of programs demonstrating that it is both scalable and provides significantly better information over the common syntactic approach and better information than lightweight closure conversion. In fact, it yields the theoretical upper-bound for many programs.

For caller-provided environments, deciding how to transform the program based on these revealed facts is also non-trivial and has the potential to incur extra runtime cost over standard strategies. We discuss how to make these decisions in a way that avoids the extra costs and how to transform a program accordingly. We also propose other uses of the analysis results beyond enabling caller-provided environments. We evaluate our transformation using an instrumented interpreter, showing that our approach is effective in reducing dynamic allocations for environments.


title: Multi-stage Programming with Splice Variables

authors:
Tsung-Ju Chiang
Ningning Xie

abstract: Multi-stage programming is a popular approach to typed meta-programming, reducing abstraction overhead and producing performant programs. However, the traditional quote-and-splice staging syntax, as introduced by Rowan Davies in 1996, can introduce complexities in managing expression evaluation, and also often necessitates sophisticated mechanisms for advanced features such as code pattern matching. This paper introduces λ○▷, a novel staging calculus featuring let-splice bindings, a construct that explicitly binds splice expressions to splice variables, providing flexibility in managing, sharing, and reusing splice computations. Inspired by contextual modal type theory, our type system associates types with a typing context to capture variables dependencies of splice variables. We demonstrate that this mechanism seamlessly scales to features like code pattern matching, by formalizing λ○▷, an extension of λ○▷pat with code pattern matching and rewriting. We establish the syntactic type soundness of both calculi. Furthermore, we define a denotational semantics using a Kripke-style model, and prove adequacy results. All proofs have been fully mechanized using the Agda proof assistant.


title: A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free

authors:
Cyril Cohen
Kazuhiko Sakaguchi

abstract: We present a novel characterization of stable mergesort functions using relational parametricity, and show that it implies the functional correctness of mergesort. As a result, one can prove the correctness of several variations of mergesort (e.g., top-down, bottom-up, tail-recursive, non-tail-recursive, smooth, and non-smooth mergesorts) by proving the characteristic property for each variation. Thanks to our characterization and the parametricity translation, we deduced the correctness results, including stability, of various implementations of mergesort for lists, including highly optimized ones, in the Rocq Prover (formerly the Coq Proof Assistant).


title: Almost Fair Simulations

authors:
Arthur Correnson
Iona Kuhn
Bernd Finkbeiner

abstract: It is well known that liveness properties cannot be proven using standard simulation arguments. This issue has been mitigated by extending standard notions of simulation for transition systems to fairness-preserving simulations for systems equipped with an additional fairness condition modeling liveness assumptions and/or liveness requirements. In the context of automated verification of finite-state systems, proofs by simulation are an appealing method as there exist efficient algorithms to find a simulation between two systems. However, applications of fair simulation to interactive verification have been much less studied. Perhaps one reason is that the definitions of fair simulation relations typically involve non-trivial nestings of inductive and coinductive relations, making them particularly difficult to use and to reason about. In this paper, we argue that in many cases, stronger notions of fair simulation involving more controlled alternations of fixed points are sufficient. Starting from known fair simulation techniques, we progressively build up a family of almost fair simulation relations for transition systems equipped with a Büchi fairness condition. The simulation relations we present can all be equipped with intuitive reasoning rules, leading to elegant deductive systems to prove fair trace inclusion. We mechanized our simulation relations and their associated deductive systems in the Rocq proof assistant, proved their soundness, and we demonstrate their use through a selection of examples.


title: Truly Functional Solutions to the Longest Uptrend Problem (Functional Pearl)

authors:
Alexander Dinges
Ralf Hinze

abstract: Solutions to the longest increasing subsequence problem are typically implemented imperatively, relying on arrays for constant-time lookups and updates. Replacing these arrays with functional sequences allows a purely functional solution with the same asymptotic running time, but with significantly worse practical performance. In this pearl, we present a purely functional approach that is not only asymptotically optimal, but also efficient in practice. The core idea is to exploit the interplay between search, lookup, and update operations through Huet's zipper. In addition, we improve the adaptive behaviour of imperative solutions commonly found in the literature.


title: Linear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)

abstract: We construct a linear type system inside dependent type theory. For this, we equip the output type of a program with a bag containing copies of each of the input variables. We call the number of copies of an input variable its multiplicity. We then characterise a dependent type which ensures that a program uses exactly the given multiplicity of each input variable. While our system is not closed under linear function types, we can program in the resulting system in a practical way using usual dependent functions, which we demonstrate by constructing standard programs on lists such as folds, unfolds and sorting algorithms. Since our linear type system is deeply embedded in a functional language, we can moreover dynamically compute multiplicities, which allows us to capture that a program uses a varying number of copies of some input depending on the other inputs. We can thereby give precise types to many functional programs that cannot be typed in systems with static multiplicities.


title: Call-Guarded Abstract Definitional Interpreters

abstract: Over the last 15 years, several popular systematic abstraction frameworks have emerged---frameworks that allow a static analysis to be derived by systematically transforming a concrete semantics. These frameworks guarantee computability of the resulting artifact by the application of an a priori abstraction which induces a particular finitization in the execution space. While effective, this abstraction occurs without regard for program structure, subjecting each program point to the same fixed degree of context sensitivity. In this paper, we present CGADI, an enhancement to systematic abstraction frameworks based on definitional interpreters which defers abstraction until a parameterized safety property signals that it should be applied. We then examine this enhanced framework instantiated with two such safety properties: a simple reentrancy property which detects non-recursive portions of program execution, and a size change property which detects evaluation paths destined to converge by virtue of appropriately decreasing values along them. The result is that CGADI can operate in the fully-precise concrete space for portions of execution without forfeiting computability. Our evaluation demonstrates that CGADI is able to produce a higher number of precise results than a corresponding CFA at relatively low cost and that, with no special treatment, CGADI can handle many programming patterns targeted by specific analysis techniques.


title: Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach

authors:
Marcos Grandury
Aleksandar Nanevski
Alexander Gryzlov

abstract:
Verifying graph algorithms has long been considered challenging in separation logic, mainly due to structural sharing between graph subcomponents. We show that these challenges can be effectively addressed by representing graphs as a partial commutative monoid (PCM), and by leveraging structure-preserving functions (PCM morphisms), including higher-order combinators.

PCM morphisms are important because they generalize separation logic's principle of local reasoning. While traditional framing isolates relevant portions of the heap only at the top level of a specification, morphisms enable contextual localization: they distribute over monoid operations to isolate relevant subgraphs, even when nested deeply within a specification.

We demonstrate the morphisms' effectiveness with novel and concise verifications of two canonical graph benchmarks: the Schorr-Waite graph marking algorithm and the union-find data structure.


title: Polynomial-Time Program Equivalence for Machine Knitting

authors:
Nathan Hurtig
Jenny Han Lin
Thomas S. Price
Adriana Schulz
James McCann
Gilbert Louis Bernstein

abstract: We present an algorithm that canonicalizes the algebraic representations of the topological semantics of machine knitting programs. Machine knitting is a staple technology of modern textile production where hundreds of mechanical needles are manipulated to form yarn into interlocking loop structures. Our semantics are defined using a variant of a monoidal category, and they closely correspond to string diagrams. We formulate our canonicalization as an Abstract Rewriting System (ARS) over words in our category, and prove that our algorithm is correct and runs in polynomial time.


title: Robust Dynamic Embedding for Gradual Typing

authors:
Koen Jacobs
Matías Toro
Nicolas Tabareau
Éric Tanter

abstract:
Gradual typing has long been advocated as a means to bridge the gap between static and dynamic typing disciplines, enabling a range of use cases such as the gradual migration of existing dynamically typed code to more statically typed code, as well as making advanced static typing disciplines more accessible. To assess whether a given gradual language can effectively support these use cases, several formal properties have been proposed, most notably the refined criteria set forth by Siek et al. One criterion asserts that the dynamic extreme of the spectrum should be expressible in the gradual language, formalized by the existence of an adequate embedding from the corresponding dynamic language.

We observe that the existing dynamic embedding criterion does not capture the desirable property of being able to ascribe embedded code to a static type that it semantically satisfies, and ensure reliable interactions with other components within the gradual language. Specifically, we introduce the notion of robustness for gradual terms, meaning that when interacting with any gradual context, runtime failures that may occur ought to be caused by the context, not by the robust term itself. We then formulate the robust dynamic embedding criterion: if a dynamic component semantically satisfies a given static type, then its embedding subsequently ascribed to that static type should be a robust term. We demonstrate that robust dynamic embedding is not implied by any existing metatheoretical property from the literature, and is not upheld by various existing gradual languages. We show that robust dynamic embedding is achievable with a gradualized simply-typed language. All the results are formalized in the Rocq proof assistant. This novel criterion complements the set of criteria for gradual languages and opens several venues for further exploration, in particular for typing disciplines that enforce rich semantic properties.


title: Normalization by Evaluation for Non-cumulativity

authors:
Shengyi Jiang
Jason Z. S. Hu
Bruno C. d. S. Oliveira

abstract:
Normalization by evaluation (NbE) based on an untyped domain model is a convenient and powerful way to normalize terms to their βη normal forms. It enables a concise technical setup and simplicity for mechanization. Nevertheless, to date, untyped NbE has only been studied for cumulative universe hierarchies, and its correctness proof critically relies on the cumulativity of the system. Therefore, we are faced with the question: whether untyped NbE applies to a non-cumulative universe hierarchy? Because such a universe hierarchy is also widely used by proof assistants like Agda and Lean, this question is of practical significance.

Our work answers this question positively. One important property typically induced from non-cumulativity is uniqueness: every term has a unique type. To faithfully reflect the uniqueness property, we work with a Martin-L'of type theory with explicit universe levels ascribed in the syntactic judgments. On the semantic side, universe levels are also explicitly managed, which leads to more complex semantics compared with a cumulative universe hierarchy. We prove that the NbE algorithm is sound and complete, and confirm that NbE does work with non-cumulativity. Moreover, to better align with common practice, we also show that the explicit annotations of universe levels, though technically useful, are logically redundant: NbE remains applicable without these annotations. As such, we provide a mechanized foundation with NbE for non-cumulativity.


title: Type Theory in Type Theory using a Strictified Syntax

authors:
Ambrus Kaposi
Loïc Pujet

abstract:
The metatheory of dependent types has seen a lot of progress in recent years. In particular, the development of categorical gluing finally lets us work with semantic presentations of type theory (such as categories with families) to establish fundamental properties of type theory such as canonicity and normalisation.

However, proofs by gluing have yet to reach the stage of computer formalisation: formal proofs for the metatheory of dependent types are still stuck in the age of tedious syntactic proofs. The main reason for this is that semantic presentations of type theory are defined using sophisticated indexed inductive types, which are especially prone to "transport hell".

In this paper, we introduce a new technique to work with CwFs in intensional type theory without getting stuck in transport hell. More specifically, we construct an alternative presentation of the initial CwF which encodes the substitutions as metatheoretical functions. This has the effect of strictifying all the equations that are involved in the substitution calculus, which greatly reduces the need for transports.

As an application, we use our strictified initial CwF to give a short and elegant proof of canonicity for a type theory with dependent products and booleans with large elimination. The resulting proof is fully formalised in Agda.


title: Fulls Seldom Differ

authors:
Mark Koch
Alan Lawrence
Conor McBride
Craig Roy

abstract: Many programs process lists by recursing in a wide variety of sequential and/or divide-and-conquer patterns. Reasoning about the correctness and completeness of these programs requires reasoning about the lengths of the lists, techniques for which are typically undecidable or at least NP-complete. In this paper we show how introducing a relatively simple (sub-)language for expressions describing list lengths, whilst not completely general, covers a great number of these patterns. It includes not only doubling but also exponentiation (iterated doubling), and moreover admits a simple length-checking algorithm that is complete over a predictable problem domain. We prove termination of the algorithm via category-theoretic pullbacks, formalized in Agda, as well as providing a more realistic implementation in Rocq, and a toy language Fulbourn with interpreter in Haskell.


title: Type Universes as Kripke Worlds

authors:
Paulette Koronkevich
William J. Bowman

abstract:
What are mutable references; what do they mean? The answers to these questions have spawned lots of important theoretical work and form the foundation of many impactful tools. However, existing semantics collapse a key distinction: which allocations does a reference depend on?

In this paper, we deconstruct the space of mutable higher-order references. We formalize a novel distinction—splitting the design space of references not only into higher-order vs (full-)ground references, but also dependency of an allocation on past vs future allocations. This distinction is fundamental to a thorny issue that arises in constructing semantic models of mutable references—the type-world circularity. The issue disappears for what we call predicative references, those that only quantify over past, not future, allocations, and for non-higher-order impredicative references. We design a syntax and semantics for each point in our newly described space. The syntax relies on a type universe hierarchy, à la dependent type theory, to kind the types of allocated terms, and stratify allocations. Each type universe corresponds to a semantic Kripke world, giving a lightweight syntactic mechanism to design and restrict heap shapes. The semantics bear a resemblance to work on regions, and suggest some connection between universe systems and regions, which we describe in some detail.


title: Compiling with Generating Functions

authors:
Jianlin Li
Yizhou Zhang

abstract: We present a new approach to scaling exact inference for probabilistic programs, using generating functions (GFs) as a compilation target. Existing methods that target representations like binary decision diagrams (BDDs) achieve strong state-of-the-art results. We show that a compiler targeting GFs can be similarly competitive—and, in some cases, more scalable—on a range of inference problems where BDD-based methods perform well. We present a formal model of this compiler, providing the first definition of GF compilation for a functional probabilistic language. We prove that this compiler is correct with respect to a denotational semantics. Our approach is implemented in a probabilistic programming system and evaluated on a range of inference problems. Our results establish GF compilation as a principled and powerful paradigm for exact inference: it offers strong scalability, good expressiveness, and a solid theoretical foundation.


title: Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs

authors:
Kwing Hei Li
Alejandro Aguirre
Simon Oddershede Gregersen
Philipp G. Haselwarter
Joseph Tassarotti
Lars Birkedal

abstract: We present Coneris, the first *higher-order concurrent separation logic* for reasoning about error probability bounds of higher-order concurrent probabilistic programs with higher-order state. To support modular reasoning about concurrent (non-probabilistic) program modules, state-of-the-art program logics internalize the classic notion of linearizability within the logic through the concept of *logical atomicity*. Coneris extends this idea to probabilistic concurrent program modules. Thus Coneris supports modular reasoning about probabilistic concurrent modules by capturing a novel notion of *randomized logical atomicity* within the logic. To do so, Coneris utilizes *presampling tapes* and a novel *probabilistic update modality* to describe how state is changed probabilistically at linearization points. We demonstrate this approach by means of smaller synthetic examples and larger case studies. All of the presented results, including the meta-theory, have been mechanized in the Rocq proof assistant and the Iris separation logic framework.


title: CRDT Emulation, Simulation, and Representation Independence

authors:
Nathan Liittschwager
Jonathan Castello
Stelios Tsampas
Lindsey Kuper

abstract:
Conflict-free replicated data types (CRDTs) are distributed data structures designed for fault tolerance and high availability. CRDTs have historically been taxonomized into state-based CRDTs, in which replicas apply updates locally and periodically broadcast their state to other replicas over the network, and operation-based (or op-based) CRDTs, in which every state-updating operation is individually broadcast. In the literature, state-based and op-based CRDTs are considered equivalent due to the existence of algorithms that let them emulate each other, and verification techniques and results that apply to one kind of CRDT are said to apply to the other thanks to this equivalence. However, what it means for state-based and op-based CRDTs to emulate each other has never been made fully precise. Emulation is nontrivial since state-based and op-based CRDTs place different requirements on the underlying network with regard to both the causal ordering of message delivery, and the granularity of the messages themselves.

We specify and formalize CRDT emulation in terms of simulation by modeling CRDTs and their interactions with the network as transition systems. We show that emulation can be understood as weak simulations between the transition systems of the original and emulating CRDT systems, thus closing a gap in the CRDT literature. We precisely characterize which properties of CRDT systems are preserved by our weak simulations, and therefore which properties can be said to be preserved by emulation algorithms. Finally, we leverage our emulation results to obtain a general representation independence result for CRDTs: intuitively, clients of a CRDT cannot tell whether they are interacting with a state-based or op-based CRDT in particular.


title: First-Order Laziness

authors:
Anton Lorenzen
Daan Leijen
Wouter Swierstra
Sam Lindley

abstract: In strict languages, laziness is typically modeled with explicit thunks that defer a computation until needed and memoize the result. Such thunks are implemented using a closure. Implementing lazy data structures using thunks thus has several disadvantages: closures cannot be printed or inspected during debugging; allocating closures requires additional memory, sometimes leading to poor performance; reasoning about the performance of such lazy data structures is notoriously subtle. These complications prevent wider adoption of lazy data structures, even in settings where they should shine. In this paper, we introduce lazy constructors as a simple first-order alternative to lazy thunks. Lazy constructors enable the thunks of a lazy data structure to be defunctionalized, yielding implementations of lazy data structures that are not only significantly faster but can easily be inspected for debugging.


title: Functional Networking for Millions of Docker Desktops (Experience Report)

authors:
Anil Madhavapeddy
David J. Scott
Patrick Ferris
Ryan Gibb
Thomas Gazagnaire

abstract: Docker is a developer tool used by millions of developers to build, share and run software stacks. The Docker Desktop clients for Mac and Windows have long used a novel combination of virtualisation and OCaml unikernels to seamlessly run Linux containers on these non-Linux hosts. We reflect on a decade of shipping this functional OCaml code into production across hundreds of millions of developer desktops, and discuss the lessons learnt from our experiences in integrating OCaml deeply into the container architecture that now drives much of the global cloud. We conclude by observing just how good a fit for systems programming that the unikernel approach has been, particularly when combined with the OCaml module and type system.


title: Reasoning about Weak Isolation Levels in Separation Logic

authors:
Anders Alnor Mathiasen
Léon Gondelman
Léon Ducruet
Amin Timany
Lars Birkedal

abstract: Consistency guarantees among concurrently executing transactions in local- and distributed systems, commonly referred to as isolation levels, have been formalized in a number of models. Thus far, no model can reason about executable implementations of databases or local transaction libraries providing weak isolation levels. Weak isolation levels are characterized by being highly concurrent and, unlike their stronger counterpart serializability, they are not equivalent to the consistency guarantees provided by a transaction library implemented using a global lock. Industrial-strength databases almost exclusively implement weak isolation levels as their default level. This calls for formalism as numerous bugs violating isolation have been detected in these databases. In this paper, we formalize three weak isolation levels in separation logic, namely read uncommitted, read committed, and snapshot isolation. We define modular separation logic specifications that are independent of the underlying transaction library implementation. Historically, isolation levels have been specified using examples of executions between concurrent transactions that are not allowed to occur, and we demonstrate that our specifications correctly prohibit such examples. To show that our specifications are realizable, we formally verify that an executable implementation of a key-value database running the multi-version concurrency control algorithm from the original snapshot isolation paper satisfies our specification of snapshot isolation. Moreover, we prove implications between the specifications—snapshot isolation implies read committed and read committed implies read uncommitted—and thus the verification effort of the database serves as proof that all of our specifications are realizable. All results are mechanized in the Rocq proof assistant on top of the Iris separation logic framework.


title: Teaching Software Specification (Experience Report)

authors:
Cameron Moy
Daniel Patterson

abstract: A course on software specification deserves a prominent place in the undergraduate curriculum. This report describes our experience teaching a first-year course that places software specification front and center. In support of the course, we created a pedagogic programming language with a focus on contracts and property-based testing. Assignments draw on real-world programs, from a variety of domains, that are intended to show how formal specification can increase confidence in the correctness of code. Interviews with students suggest that this approach successfully conveys how formal specification is relevant to software construction.


title: Multiple Resumptions and Local Mutable State, Directly

authors:
Serkan Muhcu
Philipp Schuster
Michel Steuwer
Jonathan Immanuel Brachthäuser

abstract: While enabling use cases such as backtracking search and probabilistic programming, multiple resumptions have the reputation of being incompatible with efficient implementation techniques, such as stack switching. This paper sets out to resolve this conflict and thus bridge the gap between expressiveness and performance. To this end, we present a compilation strategy and runtime system for lexical effect handlers with support for multiple resumptions and stack-allocated mutable state. By building on garbage-free reference counting and associating stacks with stable prompts, our approach enables constant-time continuation capture and resumption when resumed exactly once, as well as constant-time state access. Nevertheless, we also support multiple resumptions by copying stacks when necessary. We practically evaluate our approach by implementing an LLVM backend for the Effekt language. A performance comparison with state-of-the-art systems, including dynamic and lexical effect handler implementations, suggests that our approach achieves competitive performance and the increased expressiveness only comes with limited overhead.


title: Pushing the Information-Theoretic Limits of Random Access Lists: Traversing Cons Lists in (1 + 1/𝜎 ) ⌊lg 𝑛⌋ + 𝜎 + 9 Steps

authors:
Edward Peters
Yong Qi Foo
Michael D. Adams

abstract:
Accessing an arbitrary element of a singly linked list or cons list requires traversing up to a linear number of pointers. The applicative random-access list is a data structure that behaves like a cons list except that accessing an arbitrary element traverses only a logarithmic number of pointers. Specifically, in a list of length n, an arbitrary element can be accessed by traversing at most 3⌈lgn⌉−5 pointers.

In this paper, we present a simple variation on random-access lists that improves this bound and requires traversing at most 2⌈lg(n+1)⌉− 3 pointers. We then present a more complicated variation that improves this bound to (1+1/σ)⌊lgn⌋+σ+9 for any σ≥ 1. This shows that it is possible to get asymptotically close to the information-theoretically optimal bound of ⌈lg(n+1)⌉−1.


title: Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)

authors:
Dan Plyukhin
Xueying Qin
Fabrizio Montesi

abstract:
The past few years have seen a surge of interest in choreographic programming, a programming paradigm for concurrent and distributed systems. The paradigm allows programmers to implement a distributed interaction protocol with a single high-level program, called a choreography, and then mechanically project it into correct implementations of its participating processes. A choreography can be expressed as a λ-term parameterized by constructors for creating data “at” a process and for communicating data between processes. Through this lens, recent work has shown how one can add choreographies to mainstream languages like Java, or even embed choreographies as a DSL in languages like Haskell and Rust. These new choreographic languages allow programmers to write in applicative style (like in functional programming) and write higher-order choreographies for better modularity. But the semantics of functional choreographic languages is not well-understood. Whereas typical λ-calculi can have their operational semantics defined with just a few rules, existing models for choreographic λ-calculi have dozens of complex rules and no clear or agreed-upon evaluation strategy.

We show that functional choreographic programming is simple. Beginning with the Chorλ model from previous work, we strip away inessential features to produce a “core” model called λχ. We discover that underneath Chorλ’s apparently ad-hoc semantics lies a close connection to non-strict λ-calculi; we call the resulting evaluation strategy semilenient. Then, inspired by previous non-strict calculi, we develop a notion of choreographic evaluation contexts and a special commute rule to simplify and explain the unusual semantics of functional choreographic languages. The extra structure leads us to a presentation of λχ with just ten rules, and a discovery of three missing rules in previous presentations of Chorλ. We also show how the extra structure comes with nice properties, which we use to simplify the correspondence proof between choreographies and their projections. Our model serves as both a principled foundation for functional choreographic languages and a good entry point for newcomers.


title: Fusing Session-Typed Concurrent Programming into Functional Programming

authors:
Chuta Sano
Deepak Garg
Ryan Kavanagh
Brigitte Pientka
Bernardo Toninho

abstract:
We introduce FuSes, a Functional programming language that integrates Session-typed concurrent process calculus code. A functional layer sits on top of a session-typed process layer. To generate and reason about open session-typed processes, the functional layer uses the contextual box modality extended with linear channel contexts. Due to the fundamental differences between the operational semantics of the functional layer and the concurrent semantics of processes, we bridge the two layers using a set of primitives to run and observe the behavior of closed processes within the functional layer. In addition, FuSes supports code analysis and manipulation of open session-typed process code. To showcase its benefit to programmers we implement well-known optimizations as type-safe metaprograms over concurrent processes such as batch optimizations.

Our technical contributions include a type system for FuSes, an operational semantics, a proof of its type safety, and its implementation.


title: Formal Semantics and Program Logics for a Fragment of OCaml

authors:
Remy Seassau
Irene Yoon
Jean-Marie Madiot
François Pottier

abstract: This paper makes a first step towards a formal definition of OCaml and a foundational program verification environment for OCaml. We present a formal definition of OLang, a nontrivial sequential fragment of OCaml, which includes first-class functions, ordinary and extensible algebraic data types, pattern matching, references, exceptions, and effect handlers. We define the dynamic semantics of OLang as a monadic interpreter. This interpreter runs atop a custom monad where computations are internally represented as trees of operations and equipped with a small-step semantics. We define two program logics for OLang. A stateless Hoare Logic allows reasoning about so-called "pure" programs; an Iris-based Separation Logic allows reasoning about arbitrary programs. We present the construction of the two logics as well as some examples of their use.


title: Correctness Meets Performance: From Agda to Futhark

authors:
Artjoms Sinkarovs
Troels Henriksen

abstract: In this paper we demonstrate a technique for developing high performance applications with strong correctness guarantees. Using a theorem prover, we derive a high-level specification of the application that includes correctness invariants of our choice. After that, within the same theorem prover, we implement an extraction of the specified application into a high-performance language of our choice. Concretely, we are using Agda to specify a framework for automatic differentiation (reverse mode) that is focused on index-safe tensors. This framework comes with an optimiser for tensor expressions and the ability to translate these expressions into Futhark. We specify a canonical convolutional neural network within the proposed framework, compute the derivatives needed for the training phase and then demonstrate that the generated code approaches the performance of TensorFlow code when running on a GPU.


title: Effectful Lenses: There and Back with Different Monads

authors:
Ruifeng Xie
Tom Schrijvers
Zhenjiang Hu

abstract:
Bidirectional transformations (BXs) are a widely adopted approach for data synchronisation that is usually based on two functions, one from the source to the view and one back. Traditionally, these functions must not have side effects. While a few frameworks aim to lift this restriction by introducing monads into lenses, they are still quite limited, e.g., allowing only side effects in the backwards transformation.

In this paper, we propose a much more general framework for effectful lenses. Our effectful lenses can have different effects in their two directions, and the effects need not be cancellable. We also define the round-trip relations and use them to generalise the two well-known round-trip properties to effectful lenses. Moreover, composition preserves the two well-known round-trip properties, and we also provide a rich combinator language, which enables compositional programming for effectful lenses. Finally, we present a case study to illustrate the flexibility and expressivity of our framework.


title: Misquoted No More: Securely Extracting F* Programs with IO

authors:
Cezar-Constantin Andrici
Abigail Pribisova
Danel Ahman
Catalin Hritcu
Exequiel Rivas
Théo Winterhalter

abstract: Shallow embeddings that use monads to represent effects are popular in proof-oriented languages because they are convenient for formal verification. Once shallowly embedded programs are verified, they are often extracted to mainstream languages like OCaml or C and linked into larger codebases. The extraction process is not fully verified because it often involves quotation—turning the shallowly embedded program into a deeply embedded one—and verifying quotation remains a major open challenge. Instead, some prior work obtains formal correctness guarantees using translation validation to certify individual extraction results. We build on this idea, but limit the use of translation validation to a first extraction step that we call relational quotation and that uses a metaprogram to construct a typing derivation for the given shallowly embedded program. This metaprogram is simple, since the typing derivation follows the structure of the original program. Once we validate that the typing derivation is valid for the original program, we pass it to a verified syntax-generation function that produces code guaranteed to be semantically related to the original program. We apply this general idea to build SEIO ★ , a framework for extracting shallowly embedded F ★ programs with IO and refinement types to a deeply embedded simply typed λ -calculus while providing formal secure compilation guarantees. Using two cross-language logical relations, we devise a machine-checked proof in F ★ that SEIO ★ guarantees Robust Relational Hyperproperty Preservation (RrHP), a very strong secure compilation criterion that implies full abstraction as well as preservation of trace properties and hyperproperties against arbitrary linked adversarial code. This goes beyond the state of the art in verified and certifying extraction, which so far has focused on correctness rather than security.


title: Safety First: How to Safely Disregard Unsafe Behaviour in Compiler Calculations

abstract: Compiler calculation is a technique for deriving a correct-by-construction compiler from the specification of the compiler's correctness. In this setting, the compiler specification typically states that the semantics of each compiled program is bisimilar to the semantics of the original source program, i.e. both programs have the same behaviour. However, full bisimilarity for all source programs is too strong a requirement for complex source languages with unsafe behaviour for which the compiler need not make any guarantees, e.g. because programs that exhibit unsafe behaviour are ruled out by the type checker. This has long been recognised and exploited in compiler verification, but to date no calculation technique can handle such partial specifications. To address this, we propose a generalisation of bisimilarity, called skew bisimilarity , that allows us to weaken the compiler specification so that we may safely ignore unsafe behaviour when calculating a compiler for the specification. We demonstrate that skew bisimilarity enables us to derive compilers that produce more efficient code compared to previous compiler calculation techniques, all while maintaining the same strong correctness guarantees for safe source programs. We further show that – even for source languages without unsafe behaviour – skew bisimilarity provides a powerful generalisation of bisimilarity that enables a novel calculation technique for reasoning about register machines. This improves on existing compiler calculation techniques for register machines, which are currently limited to terminating source languages without effects. To demonstrate the effectiveness of skew bisimilarity as a proof technique for compiler calculation, we have fully formalised it in Agda and used this formalisation to calculate compilers for a variety of languages, including the first calculation of a compiler for a typed concurrent lambda calculus that targets a register machine.


title: Inlining as a Space Optimization: A Simple Time- and Space-Invariant Implementation of the Weak Lambda-Calculus

abstract: We propose an implementation model for the evaluation of the weak λ -calculus, which is invariant for both time and space complexity, in both call-by-name and call-by-value strategies. In other words, this model provides an implementation of any weak call-by-name or weak call-by-value λ -calculus reduction sequence, whose time complexity is polynomial in the number of simulated β -steps, and whose space complexity is linear in the size of the largest intermediate term. This solves in an elegant way the well-known tension between time-invariance and space-invariance in the implementation of the λ -calculus.


title: When Types Intersect and Effects Get Handled

authors:
Stefano Catozi
Ugo Dal Lago
Taro Sekiyama

abstract: We introduce a novel intersection type system for a λ -calculus with algebraic effects and handlers. The system, inherently behavioral in nature, enjoys the classical properties of intersection type systems, in particular subject reduction and expansion . It thus characterizes the set of terms whose evaluation process terminates and, at the same time, allows reducing the reachability problem to type inference. This new system, the first with these features for a calculus with handlers, induces a system of simple types which, although not guaranteeing termination, is type sound and admits a decidable HOMC problem, unlike similar type systems like Dal Lago and Ghyselen's HEPCF .


title: A Catenable, Splittable, Transient Sequence Data Structure

authors:
Arthur Charguéraud
François Pottier

abstract: A transient data structure is a combination of an ephemeral data structure, a persistent data structure, and fast conversions between them. We present a transient sequence data structure that supports efficient read and write access at an arbitrary index with worst-case time complexity O ( K log K n ), pushing and popping at either end with complexity O ( K log K n ), and splitting and concatenation with complexity O K log K n + log K 2 n , where K is a user-defined chunk size and n is the length of the sequence. We provide a detailed analysis of this data structure and show that, in many favorable scenarios, it performs much better than these pessimistic bounds might suggest. Furthermore, we describe its implementation, and provide a synthetic benchmark to evaluate the performance of push and pop . We believe that it is a good candidate for a one-size-fits-all, general-purpose sequence data structure.


title: QuickChecking Convergence of Rewriting Systems (Functional Pearl)

abstract: Term rewriting systems are a common tool in automated reasoning and semantics of programming languages, and many practical applications require these systems to be convergent. While automated tools and theory exist to establish convergence, this paper is concerned with a practical method for testing it to quickly find useful counterexamples. Standard property-based testing approaches struggle here: exhaustively computing all normal forms is fundamentally flawed and too slow, while generating random normal forms makes counterexample minimization (shrinking) fragile due to dependencies on earlier generated test data. To solve this, we introduce a QuickCheck testing method based on generating and shrinking random execution traces. By checking if the first and last terms of a generated trace share the same deterministic normal form, we remove the data dependency between generators. This approach yields a property that efficiently finds counterexamples and enables fast, robust shrinking. We demonstrate the effectiveness of this method on various examples, ranging from group theory equations to distributed process calculus.


title: LazyHMC: Hamiltonian Monte Carlo Simulation for Lazy, Infinite Dimensional Probabilistic Programs

authors:
Maria-Nicoleta Craciun
C.-H. Luke Ong
Tom Schrijvers
Sam Staton

abstract: Hamiltonian Monte Carlo (HMC) is a successful generic inference method in probabilistic programming, but in its ordinary formulation it needs gradients and finite-dimensional parameter spaces. In Haskell, lazy evaluation lets probabilistic programs express stochastic processes and other non-parametric Bayesian models over implicit infinite-dimensional spaces. This paper develops new formulations of gradient-based HMC for this infinite-dimensional setting, via lazy evaluation. For automatic differentiation, we provide an analysis based on a new notion of “piecewise analytic under cylindrical analytic partition” (PACAP), to show that even if a program is infinite-dimensional and defined lazily, the gradient of the likelihood function is finitely supported. For the Monte Carlo method itself, we develop several HMC variants and a No-U-Turn Sampler that operate over the infinite-dimensional parameter space but are still productive because of lazy evaluation. Experiments cover Gaussian mixture clustering, random walks, and piecewise-constant regression with Poisson-process changepoints.


title: Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice

authors:
Matthew L. Daggitt
Ekaterina Komendantskaya
Alistair Sirman
Alessandro Bruni
Samuel Teuber
Josh Smart
Grant O. Passmore

abstract: Formal verification of neuro-symbolic cyber-physical systems, such as drones, medical devices and robots, is complicated. Neural components must be trained to be optimal with respect to the available data as well as the safety specifications, and then verified using specialised solvers. Symbolic models of the “cyber” and “physical” behaviour of the system must be constructed and verified in interactive theorem provers (ITPs), often requiring mature mathematical libraries to reason about the interplay of discrete and continuous dynamics, preferably obtaining infinite time-horizon guarantees. Finally, the results of the two already challenging verification tasks need to be integrated into a single proof. In this paper we present a compositional methodology for constructing such proofs. The Vehicle framework provides a functional, domain-specific language for specifying, training, and verifying neural components. We extend Vehicle to allow integration with any ITP with minimal effort, thereby bridging the gap between the neural and symbolic proofs. First, we describe how Vehicle ’s standard bidirectional type checker can be reused to transpile neural specifications into an intermediate representation targeting multiple theorem provers. Second, we integrate Vehicle with Rocq, Isabelle/HOL, Agda and the industrial prover Imandra; and showcase a generic infinite time-horizon safety proof of a discrete cyber-physical system with a neural network controller in each ITP. Finally, to put the idea of compositional neural-cyber-physical system verification to the test, we use the Mathematical Components libraries in Rocq to verify infinite time-horizon safety of a medical device, modelled as a continuous cyber-physical system with a neural controller. To our knowledge, this is the first result of this kind in a general purpose ITP; and a result that was only feasible thanks to the compositionality provided by Vehicle ’s functional interface.


title: On Recursion in Graded Modal Type Theory

authors:
Oskar Eriksson
Andreas Abel
Nils Anders Danielsson

abstract: We present a graded modal type theory with recursion over natural numbers and prove formally in Agda that it handles resources correctly, in the sense that an abstract machine accesses resources the “correct” number of times. The theory is parametrized, and can for instance be instantiated with grades for erasure, linear types, or affine types. The correctness proof shows that our usage counting is sound. Our eliminator for natural numbers is flexible as it enables different resource-usage patterns and practical in the sense that it can be used both to define functions with expected usage counts for the arguments. Further, it can be used to encode other data types, using large elimination. Finally, we adapt our resource correctness proof to show correctness also for grades tracking information flow, in the form of a non-interference property.


title: Confluence Techniques for Dependent Type Theory with Typed Conversion

authors:
Thiago Felicissimo
Théo Winterhalter

abstract: In the meta-theoretic study of dependent type theory, confluence techniques are powerful tools for establishing the properties required when proving correctness of implementations. Unfortunately, such techniques have historically mostly been studied for type theories with untyped conversion, which are harder to relate to semantics. In thiswork,we showhowto scale confluence techniques to rich dependent type theories with typed conversion. To do this, we prove a confluence theorem for a theory featuring not only function types (without η ) and universes, but also some inductive types (Nat and sums), dependent pairs (without η ), definitional proof irrelevance and a lift type (with η ), allowing to simulate a weak form of explicit cumulativity (as done in Agda ). We then show how to extend our framework with a definitionally proof-irrelevant equality in two ways, either with an observational equality or with an eliminator with a non-linear computation rule (as done in Lean ), illustrating the extensibility of our approach. With confluence in hand, we then fulfill our promise of showing (partial) correctness of type- and conversion-checking algorithms. Moreover, while our specification for the type theory is fully annotated, which eases the connection with semantics, we prove correctness of algorithms that operate on usual non-annotated terms, an important optimization for real-life implementations. Finally, our results have been fully formalized in Rocq and can serve as a basis for future type theory formalizations.


title: Animated Pictures for Slide Presentations: From the Shallows to the Depths of a Domain-Specific Language (Functional Pearl)

authors:
Oliver Flatt
Robert Bruce Findler
Matthew Flatt

abstract: Another DSL for pictures? Seems fishy. But hold fast as we chart a course to an embedded DSL for the domain of slide presentations with animations. Our DSL programs interact with the host language in two ways: by allowing pictures and animations to be built using host-language functions (resembling a shallow embedding), and by allowing host-language reflection on their construction (resembling a deep embedding). As a result, users can define their own animation combinators but still also inspect, adjust, and reassemble animations. To demonstrate our DSL’s expressive power, we show how it supports a Keynote-like Magic Move operation. Having made the DSL shipshape, we dive into a lesson learned about deep and shallow DSL design. While deep and shallow may seem like mutually exclusive options, we argue they are actually points on an entire spectrum of possible DSL designs. More importantly, our paper demonstrates that points on the spectrum between deep and shallow are where DSL designs achieve full sail.


title: An Equational and Graphical Fixed-Point Calculus (Functional Pearl)

authors:
Gustavo de Mendonça Freire
Hugo Musso Gualandi
Hugo Nobrega
Joao Paixao

abstract: The fixed-point calculus is a toolbox of theorems for reasoning equationally about fixed points. However, the underlying concepts of the calculus are not defined equationally, including the central definition, that of least fixed point. Thus, although the key theorems of the fixed-point calculus are equational, their proofs are not. In this work, we give equational specifications for the main concepts of the fixed-point calculus for partially ordered sets, to allow more proofs to be written in an equational style. Since reasoning equationally can be cumbersome without appropriate abstractions, we employ the graphical language of string diagrams, based on a category of feasibility relations, to make reasoning more ergonomical. Our contributions culminate in graphical equational proofs of key results of the fixed-point calculus, including the rolling, diagonal, and square rules; fixed-point fusion; and the mutual recursion theorem.


title: Package Managers à la Carte: A Formal Model of Dependency Resolution

authors:
Ryan Thomas Gibb
Patrick Ferris
David Allsopp
Thomas Gazagnaire
Anil Madhavapeddy

abstract: Package managers are legion. Every programming language and operating system has its own solution, each with subtly different semantics for dependency resolution. This fragmentation prevents multilingual projects from expressing precise dependencies across language ecosystems; it leaves external system dependencies implicit and unversioned; and it obscures the full dependency graph that supply-chain analysis depends on. We present the Package Calculus , a formalism for dependency resolution that unifies the core semantics of package managers. Through a series of formal reductions, we show how this core is expressive enough to model the diversity of real-world dependency expression languages. The calculus provides the theoretical foundation for future cross-ecosystem tooling, as a lingua franca of dependency expression.


title: Towards a Higher-Order Bialgebraic Denotational Semantics

authors:
Sergey Goncharov
Marco Peressotti
Stelios Tsampas
Henning Urbat
Stefano Volpe

abstract: The bialgebraic abstract GSOS framework by Turi and Plotkin provides an elegant categorical approach to modelling the operational and denotational semantics of programming and process languages. In abstract GSOS, bisimilarity is always a congruence, and it coincides with denotational equivalence. This saves the language designer from intricate, ad-hoc reasoning to establish these properties. The bialgebraic perspective on operational semantics in the style of abstract GSOS has recently been extended to higher-order languages, preserving compositionality of bisimilarity. However, a categorical understanding of bialgebraic denotational semantics according to Turi and Plotkin’s original vision has so far been missing in the higher-order setting. In the present paper, we develop a theory of adequate denotational semantics in higher-order abstract GSOS. The denotational models are parametric in an appropriately chosen semantic domain in the form of a locally final coalgebra for a behaviour bifunctor, whose construction is fully decoupled from the syntax of the language. Our approach captures existing accounts of denotational semantics such as semantic domains built via general step-indexing, previously introduced on a per-language basis, and is shown to be applicable to a wide range of different higher-order languages, e.g. simply typed and untyped languages, or languages with computational effects such as probabilistic or non-deterministic branching.


title: Completeness of Iris-Based Program Logics

authors:
Johannes Hostert
Zichen Zhang
Puming Liu
Simon Oddershede Gregersen
Ralf Jung
Joseph Tassarotti

abstract: Traditionally, proof systems such as program logics come with two core theorems: soundness and completeness . The role of soundness is obvious: we want to be sure that arguments carried out inside the logic actually lead to correct conclusions. Completeness complements that by ensuring that the logic does not limit expressivity: in principle, any correct result can be obtained within the confines of the logic. This result typically has to be stated relative to the completeness of the assertion logic that is used to reason about pre- and postconditions. Over the past decade, the Iris framework has emerged as a widely used foundation for building separation logics. While Iris-based logics typically come with a soundness proof, none of them have a proof of completeness. In this paper, we present the first approach for establishing completeness of Iris-based program logics, and we show the generality of our methodology by applying it to a range of different logics described in prior work, including partial and total concurrent separation logics for a higher-order ML-like language, two quantitative logics (for bounding execution time and probabilistic errors), and a relational logic for proving refinement. All our results have been mechanized in Rocq.


title: Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report)

authors:
Eleftherios Ioannidis
Nikhil Swamy
Gabriel Ebner
Matthai Philipose
Tahina Ramananandro

abstract: The widespread adoption of AI-assisted coding is directly proportional to an increase in software bugs; can AI-assisted formal verification help reduce bugs at a comparable scale? In this experience report we give an anecdotal account of AI agents, equipped with a CLI and a proof assistant, producing thousands of lines of machine-checked code. We detail our experience across different proof-engineering tasks: implementing verified data structures for a standard library, translating unverified code into a formal language while inferring its specification, and porting and refactoring existing proofs to new frameworks. We present the techniques that made agentic proof-oriented programming (PoP) effective–or ineffective–and characterize the role of the human expert, whose contribution reduces to providing natural-language problem descriptions, reviewing auto-generated specifications, and occasionally supplying a key invariant. Our findings suggest that this division of labor provides substantial leverage to the human expert in the loop: three experts, over the course of two weeks, completed case studies whose manual proof-engineering cost we estimate at roughly half a year.


title: Demand-on-Demand Control-Flow Analysis

authors:
Chahyun Kang
Kimball Germane

abstract: Understanding program behaviors requires reasoning about control flow. Functional programs complicate this reasoning since call targets are computed in general. Control-flow analysis (CFA) can effectively reason about control flow (and much more) but is costly. Demand-driven CFA is less expensive but less versatile, and it is difficult to make it do what classical CFA does. This is unfortunate because many fundamental optimizations rely on control flow reasoning. In this paper, we present Demand-on-Demand Control-Flow Analysis (DoDCFA), a hybrid exhaustive–demand-driven CFA that recovers some of the versatility/applicability of classical CFA while improving on the speed of Demand CFA. The result is an analysis that can inexpensively and effectively analyze control flow and environment behavior sufficient to justify inlining.


title: Programmable Property-Based Testing

authors:
Alperen Keles
Justine Frank
Ceren Mert
Harrison Goldstein
Leonidas Lampropoulos

abstract: Property-based testing (PBT) is a popular technique for establishing confidence in software, where users write properties —i.e. executable specifications—that can be checked many times in a loop by a testing framework. In modern PBT frameworks, properties are usually written in shallowly embedded domain-specific languages, and their definition is tightly coupled to the way they are tested. Such frameworks often provide convenient configuration options to customize aspects of the testing process, but users are limited to precisely what library authors had the prescience to allow for when developing the framework; if they want more flexibility, they may need to write a new framework from scratch. We propose a new, deeper language for properties based on a mixed embedding that we call deferred binding abstract syntax , which reifies properties as a data structure and decouples them from the property runners that execute them. We implement this language in Rocq and Racket, leveraging the power of dependent and dynamic types, respectively. Finally, we showcase the flexibility of this new approach by implementing a variety of property runners in a shared framework, highlighting domain-specific testing improvements that can be unlocked by more programmable testing.


title: Citrus: Algebraic Reasoning about Superconductor Electronics

authors:
Harlan Kringen
Timothy Sherwood
Ben Hardekopf

abstract: We present Citrus, an embedded DSL in the dependently-typed language Agda that formalizes high-level abstractions for specifying and reasoning about superconducting electronics (SCE) circuits. We build on the existing PyLSE language, a Python DSL for writing SCE programs that provides facilities for simulating designs and for verification via model-checking (by compiling its basic structures into Timed Automata). Citrus expands on the verification capabilities of PyLSE by defining equivalence over SCE gates, as well as corresponding equational reasoning lemmas, and providing a toolbox of functional combinators for designing and analyzing larger circuits. The formalization enables a large increase in expressivity, specifically in the form of algebraic reasoning about SCE designs. We evaluate Citrus using two sets of case studies. In the first, we establish several equational laws which are often used by SCE designers but have yet to be formally proven. In the second, we prove a verification task which the PyLSE language was unable to prove due to the state space explosion inherent in its model checking approach. In this way, Citrus provides a simple functional programming language, equivalent to PyLSE, with increased verification capabilities.


title: First-Class Constrained Types: Elaboration, Type Inference, Approximation, and a Characterization of Termination

authors:
Chun Kit Lam
Florent Ferrari
Lionel Parreaux

abstract: We study a first-class treatment of constrained types, which were previously confined mostly to ML-style polymorphism. We define System FCCT, an extension of System F with polymorphic subtyping and constraint abstraction in types. A value of type c ⇒ τ can be used at type τ in any context where the subtyping constraint c can be discharged. We show that FCCT exhibits interesting properties. First, all well-typed FCCT terms terminate under call-by-name evaluation (CBN), which can be shown by elaboration into System F. Second, all CBN-terminating terms are well-typed in FCCT. Together, these two properties mean that typability in System FCCT characterizes call-by-name termination. Third, FCCT admits a principal type inference semialgorithm, called FCCT ℐ , which makes no approximations and can thus be seen as an idealized “ground truth” of type inference. We show that FCCT ℐ indirectly simulates term reduction, shedding some light on the difficulty of bounded polymorphic type inference. Finally, we extend FCCT ℐ to track abstracted call contexts and perform approximation by sharing polymorphic instantiations, ensuring termination on all input terms while preserving soundness. In addition to making the connection between polymorphic subtype constraint solving and term reduction, this paper also establishes a connection between constrained types and existing intersection type systems, which are known to characterize various normalization properties.


title: Imprecise Probabilistic Programming, Precisely: Credal Sets via Graded Monads, BDDs, and Semiring-Parametric Inference (Functional Pearl)

authors:
Jack Liell-Cock
Sam Staton

abstract: Imprecise probability generalizes standard probability theory by replacing a single distribution with a convex set of possible distributions. We show that this generalization requires no change to the standard BDD compilation and weighted model counting pipeline used by discrete probabilistic languages. An imprecise coin flip is simply a BDD variable whose weight is left free rather than fixed. We introduce I mp , a Haskell-embedded DSL for imprecise probabilistic programming. A graded monad, indexed by finite sets of named sources of epistemic uncertainty, restores the commutativity that the standard convex powerset monad lacks, and GHC’s type system enforces this at compile time. Weighted model counting is parametric in the semiring, so the same compiled BDD supports exact, differentiable, and interval-bounded inference.


title: Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types

authors:
Vilem-Benjamin Liepelt
Danielle Marshall
Dominic Orchard

abstract: Graded types provide a way to augment a type system with fine-grained information, e.g., to track side effects or context dependence and resource use (called coeffects ). Graded types for coeffects have found their way into languages such as Haskell, Idris, and Granule, enabling resourceful reasoning via coeffect analysis with varying levels of generality. Two separate lineages of graded coeffect system have emerged in the last decade: those in which coeffect annotations are pervasive, requiring annotations on function types (which we call graded-base ) and those in which coeffects are added by way of a graded modal type operator atop linear types (which we call linear-base ). The latter has its origins in Girard’s Linear Logic which has been a rich humus for programming language research focused on resources, whereas the graded-base approach emerged in the mid-2010s, seeing rapid adoption in programming language theory and practice, e.g. in QTT and Linear Haskell. The relationship between these two styles has however remained an open question. We answer this question by giving translations between pairs of calculi of both lineages that we prove type-, grade- and operational-semantics preserving. We show that the same notions of context dependence can be expressed in either style, building a bridge between the two lineages that enables transfer of results and ideas, while helping language designers to make better informed choices.


title: A Separation Logic for Parallel Time Complexity with Work and Span Credits

authors:
Alexandre Moine
Sam Westrick
Joseph Tassarotti

abstract: We present Parcas, a concurrent separation logic for verifying the parallel time complexity of fork-join programs. In order to abstract from the specifics of the machine, time complexity for parallel programs is given in terms of two metrics: the work, measuring the total number of operations, and the span, measuring the longest chain of sequential dependencies. Together, these two metrics determine the running time on any number of processors. For proving bounds on the work and span, Parcas is equipped with work credits and span credits, logical devices that represent permissions to incur costs. Work credits are a straightforward adaptation of time credits, a standard tool for bounding time complexity of sequential programs, and can be split additively between parallel tasks. Span credits, however, require a fundamentally different treatment. Indeed, the span of the parallel composition of two tasks is the maximum of the span of the two tasks. To account for this, we propose a rule for duplicating span credits at fork points, with each copy tagged by a logical task identifier that restricts which task may spend them. A transfer rule allows unused span credits to be forwarded across sequential compositions to subsequent tasks. The logic is expressive enough to give modular, higher-order specifications for common parallel primitives such as a parallel for loop and a tabulate function. We demonstrate Parcas on several case studies, including parallel prefix sums, parallel merge sort, and a variant of Treiber’s lock-free stack that mixes concurrency with parallelism. All the presented results are mechanized in the Rocq prover using the Iris separation logic framework.


title: Another Type Inference Algorithm for First-Class Implicit Polymorphism

abstract: We propose yet another approach to type inference with first-class implicit polymorphism, based on the interleaving of an Algorithm ℳ-style constraint-generating elaboration of terms and a solver for the generated constraints. The novelty of our approach is that types include explicit syntactic representations of unknown polymorphic types during type inference. Solving unification constraints with unknown polymorphic types also computes type arguments for the elaborated terms. The resulting system is uniform, simple, extends to support domain-specific constraints, and compares favorably with other approaches to first-class implicit polymorphism.


title: Unscanning by Möbius Inversion (Functional Pearl)

abstract: This pearl presents the classical Möbius inversion theorem for posets as a calculation method for inverting scan-like cumulative computations. We model a scan function as summation over principal down-sets of a lower-finite poset: local values are accumulated according to the order. From this specification, the inverse can be derived directly as a recursion. When this recursion is expanded as a linear combination of cumulative values, the coefficients obtained are precisely the Möbius coefficients of the poset. In this way, the usual theorem gives the algebraic justification, while the calculation shows where the coefficients come from in the inverse problem. We then use a cancellation law to identify the nonzero coefficients, which determines which cumulative values are actually needed in each unscan rule. Because this sparsity pattern is determined only by the indexing order, the same calculation can be reused across different data structures. We illustrate the method with five standard examples: prefix sums on lists, summed-area tables on grids, subtree sums on trees, subset sums, and divisor sums.


title: Tail Modulo Async-Await

authors:
Emma Nardino
Ludovic Henrio
Gabriel Radanne
Yannick Zakowski

abstract: This article extends tail-call optimisation by applying it to asynchronous calls. We first introduce Tail-Modulo-Await , a novel code transformation for asynchronous tail recursive functions that prevents the creation of unnecessary tasks. We then show how to combine Tail-Modulo-Await with the existing Tail-Modulo-Cons optimisation; we obtain an optimisation able to turn a recursive function with multiple tail calls under constructors into a parallel version of the function, also optimised in space. We formalise both optimisations over representative calculi, and prove them correct through backward simulations. Finally, we provide a proof-of-concept implementation as an OCaml syntax extension and evaluate it experimentally, showing our approach optimises both memory and execution time.


title: Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)

abstract: We report on using an agentic coding assistant (Claude Code, powered by Claude Opus 4.6) to mechanize a substantial Rocq correctness proof from scratch, with human guidance but without any human-authored proof code. The proof establishes semantic preservation for the administrative normal form (ANF) transformation in the CertiRocq (formerly CertiCoq) verified compiler for Rocq. The closely related continuation-passing style (CPS) transformation in CertiRocq was previously proved correct by human experts over several months. We use this proof as a template and instruct the LLM to adapt the proof technique to the ANF setting, which differs in important technical ways. The resulting ANF proof comprises approximately 6,000 lines of Rocq proof (larger than the 4,200-line CPS proof) and was developed in 94.5 hours. We describe the proof technique and report on the experience of developing it with an LLM, discussing both the strengths and limitations of the approach and its implications for verified compiler construction.


title: Mode Crossing

authors:
Benjamin Peters
Jules Jacobs
Diana Kalinichenko
Liam Stevenson
Aspen Smith
Derek Dreyer
Richard A. Eisenberg

abstract: OxCaml extends the OCaml type system with support for safe low-level systems programming via modes . For example, OxCaml's modal portability and contention axes ensure that concurrent OxCaml programs have no data races. In practice, however, mode tracking can reject programs that are obviously safe, such as when the data shared across threads is immutable. To remedy this problem, we introduce mode crossing —the ability to automatically strengthen modes (e.g., from nonportable to portable ) for values of certain types. Mode crossing significantly reduces the annotation burden associated with modal types, and we further introduce a new type system feature, modal kinds . We present a type-theoretic account of modal kinds, interpret them as monotone functions on a lattice of modes, and extend this interpretation to incorporate abstract types. We verify soundness of the modal kind system in Rocq on top of Iris. We design an inference procedure that reduces kind checking and subsumption to constraints solved by a dedicated lattice solver. Our design is implemented in a large industrial codebase, demonstrating practical usability.


title: LoCalMem: Type-Directed Adaptive Serialization for Location- and Content-Addressable Memory

authors:
Michael Rainey
Michael H. Borkowski
Michael Vollmer
Chaitanya S. Koparkar
Mikah Kainen
Vidush Singhal

abstract: Functional programming languages support non-destructive updates via structural sharing, creating a funda-mental tradeoff in memory representation: pointer-based heaps preserve sharing but degrade layout locality, while serialized heaps prioritize locality at the cost of duplication. Gibbon addresses this tradeoff by using adaptive serialization: as the program updates its heap, the memory manager improves locality through serialization, falling back to indirection where sharing is unavoidable. In this work, we formalize key parts of Gibbon’s memory model, including the statics and dynamics of adaptive serialization. We then present a unified, type-directed memory model with two realizations: location-addressable memory (LAM) for local execution and content-addressable memory (CAM) for persistence and distributed deduplication. The key abstraction in both models is a notion of explicit boundary datatypes mediating between sharing and serialization. In LAM, boundaries facilitate adaptive serialization and enable our soundness proofs. In CAM, the same boundaries enable an efficient chunking policy, whereby candidate chunk points are selected via rolling-hash cuts. We establish efficiency via a static bound on the number of tokens between consecutive boundaries, bounding reserialization costs. We work in the purely functional setting, where structural sharing is observationally transparent and content-addressed identity is well defined. We formalize both models with operational semantics and prove soundness with respect to ordinary functional values. For CAM, we prove a locality theorem: the work required for an update scales with the depth of the modified path rather than the size of the value. Consequently, large persistent values can be updated incrementally, with unchanged substructures shared automatically across versions and across machines. Together, these results show that a single boundary discipline can unify local structural sharing and distributed deduplication within one type-theoretic foundation.


title: Programming Backpropagation with Reverse Handlers for Arrows

authors:
Takahiro Sanada
Keisuke Hoshino
Kenshin Hirai
Shin-ya Katsumata

abstract: We introduce a new programming language and its categorical semantics in order to design and implement neural networks within the framework of algebraic effects and handlers for arrows. Our language enables us to construct neural networks symbolically, in the same manner as algebraic effects, and to assign implementations—such as backpropagation computations—to them via handlers. The advantage of this language design is that network descriptions become abstract and high-level, while implementations can be flexibly assigned to networks. We establish a rigorous foundation for our language by developing a type system, an operational semantics, a categorical semantics, and soundness and adequacy theorems. The technical core is the introduction of reverse handlers , a novel handler mechanism for arrows for implementing backpropagation, together with new algebras of strong promonads on reverse differential restriction categories (RDRCs), whose string diagrams provide a formal graphical syntax and semantics for neural networks.


title: Set-Theoretic Types for Erlang in Practice (Experience Report)

authors:
Albert Schimpf
Annette Bieniusa

abstract: Set-theoretic type connectives with their native support for union, intersection, and negation have the potential to capture the idioms of dynamically typed languages like Erlang. We investigate whether this theoretical expressiveness translates into practice: does the resulting type solver remain tractable on real-world code? Can the type system reflect the programmer's intention even though no principal types exist? And does it actually detect or avoid errors in real codebases? This paper reports on our experience on applying Etylizer , a set-theoretic type checker for Erlang, to its own implementation. We test whether the type system can express the patterns arising in a non-trivial Erlang codebase. In addition, we examine the design tradeoffs that set-theoretic types present across exhaustiveness, function overloading, numeric precision, gradual typing, and occurrence typing, and relate them to how other type systems handle the same dimensions. Our findings suggest that set-theoretic types are expressive enough to capture Erlang programmers' intentions: intersection types and automatic exhaustiveness checking provide clear advantages, and the approach is not in conflict with Erlang's let-it-crash idiom. Although the type system lacks principal types, types can be refined as needed through annotations. Scalability for type checking is largely addressed, and in the cases where it remains an issue, less expressive tools face similar limitations.


title: Editorial Message

abstract: The Proceedings of the ACM series presents the highest-quality research conducted in diverse areas of computer science, as represented by the ACM Special Interest Groups (SIGs). The Proceedings of the ACM on Programming Languages (PACMPL) focuses on research on all aspects of programming languages, from design to implementation and from mathematical formalisms to empirical studies. The journal operates in close collaboration with the ACM Special Interest Group on Programming Languages (SIGPLAN) and is committed to making high-quality peer-reviewed scientific research in programming languages free of restrictions on both access and use.


title: Bimodels and Biorthogonality for Abstract Machines

authors:
April Tune
G. A. Kavvos

abstract: We develop a compositional semantics for abstract machines, focusing on CK/CEK machines for call-by-push-value. Taking abstract machines as the primary operational semantics, we introduce bimodels, which give denotations to both programs and stacks, and environment bimodels, which extend the construction to closures. Each has a syntactic instance, built from the machine itself, and a set-theoretic instance that serves as a denotational semantics. Using biorthogonality, we define logical relations over these models and prove fundamental lemmata that are parametric in the choice of model and observation. Different instantiations yield canonicity, adequacy, operational extensionality, internal full abstraction, and a first-order simulation-theorem relating the CK and CEK machines. All results are mechanized in Agda.


title: Compositional Generator Equivalence

authors:
Anthony Vandikas
Kiarash Sotoudeh
Marsha Chechik

abstract: Property-based testing (PBT) is a powerful technique for software verification that relies on random input generators and “shrinking” processes to find and minimize counterexamples to executable specifications called properties. While optimizing these generators is crucial for testing efficiency, formally justifying such optimizations is currently difficult because existing languages lack a compositional semantics that is coarse-grained enough for high-level reasoning. In this paper, we first provide a formal account of the syntax and semantics of Hedgehog, a popular PBT framework. We demonstrate that Hedgehog’s distribution semantics – which models how users typically reason about generators – is non-compositional. Furthermore, we prove that any sound and complete compositional semantics for Hedgehog must necessarily be equivalent to its sampling semantics, which is too fine-grained to justify common program optimizations. To resolve this dilemma, we introduce Hedgehog ↑ , a restricted version of the language based on the arrow calculus, and prove that Hedgehog ↑ possesses a compositional distribution semantics. We evaluate Hedgehog ↑ through a Haskell implementation and show that it remains expressive enough to capture generators of practical interest, while providing the formal foundation needed for compositional generator equivalence proofs.


title: Adequacy for Predicate Transformer Semantics

authors:
Kazuki Watanabe
Mirai Ikebuchi
Mayuko Kori

abstract: Verifying effectful higher-order programs, such as probabilistic programs with unbounded recursion, is a central problem in program verification. Predicate transformer semantics, closely related to continuation-passing style and weakest precondition semantics, has been proposed as a compositional method for computing verification objectives. Due to its categorical and denotational formulation, it can uniformly capture quantitative properties such as expected costs. However, its relationship to operational semantics remains largely unexplored with respect to more advanced properties, such as cost moments and conditional expectations of probabilistic programs with unbounded recursion, thereby leaving its connection to concrete program executions unclear. In this paper, we establish a generic framework to prove adequacy for predicate transformer semantics with respect to an appropriately designed operational semantics. Our approach is simple yet expressive enough to cover a wide range of instances, including total expected costs, cost moments, conditional expectations, and expected multiplicative rewards of probabilistic higher-order programs with unbounded recursion.


title: Let It Be Optimized: Building Multi-stage Evaluators with Let-Insertion and Optimizations in Small Pieces (Functional Pearl)

authors:
Guannan Wei
Jun Tan
Dinghong Zhong

abstract: Multi-stage programming lets programmers write meta-programs that generate efficient code. Staging is typically realized either as a language primitive with quotations and splices ( e.g. , MetaML and its descendants), or as a library embedded in a host language ( e.g. , Lightweight Modular Staging). Unlike quotation-based approaches, practical library-based systems combine staged evaluation with automatic let-insertion to preserve evaluation order, along with optimizations that improve residual code. Despite their popularity and practical importance, this combination has received little semantic treatment, making it difficult to reason about correctness or to compare systematically with other staging paradigms. Using functional programming techniques, this pearl illuminates the operational aspects of staged evaluation with automatic let-insertion and optimizations as found in library-based staging systems. For a core two-stage language, we develop a series of definitional interpreters that concisely describe staged evaluation generating optimized, let-inserted residual programs. The interpreters are written in the extended continuation-passing style, where two continuations naturally account for let-insertion. With minor refactoring, we showcase a suite of optimizations, ranging from simple constant propagation/folding, common subexpression elimination, and dead-code elimination to more involved optimizations such as β -inlining, partially-static data, and code motion. Each optimization is presented as a small, modular extension integrated into staged evaluation, requiring neither additional effort from the meta-programmer, nor complex post-hoc compiler infrastructure.


title: HMCFA: A Precise and Practical Big-Step Control Flow Analysis for Effect Handlers

authors:
Tim Whiting
Kimball Germane

abstract: Effect handlers enable powerful control flow patterns by capturing and resuming continuations, but no control flow analysis exists for programs using them. Applying existing approaches for other delimited control operators would either lose precision through CPS translation or be computationally intractable. We present HMCFA, the first practical control flow analysis for effect handlers based on big-step semantics. Our key technical contributions are: (1) a big-step semantics for effect handlers that allocates denotables and continuations in an explicit store to avoid unbounded syntactic growth, enabling systematic abstraction in the style of Abstracting Definitional Interpreters (ADI); we prove this semantics equivalent to Bauer and Pretnar’s substitution-based big-step semantics. (2) A two-component timestamp that tracks both the current call context and the context in which each handler was installed, so that when an operation is dispatched to a handler, its analysis reflects the invocation context that installed it. We prove our concrete semantics equivalent to Bauer and Pretnar’s and establish soundness of our abstraction via address freshness. An evaluation on Koka benchmarks shows that our address space has good precision even without context sensitivity, but that our timestamp can close most of the remaining gap in precision while still being tractable on our benchmark suite.


title: Assertions for Free: Transferring Invariants from Algorithm to Implementation Proofs (Functional Pearl)

authors:
Shushu Wu
Chengxi Yang
Xiwei Wu
Qinxiang Cao

abstract: Verifying the functional correctness of real-world code with complex algorithms can be decomposed into two layers: verifying that the concrete code refines an abstract algorithmic description, and proving the correctness of the formal description. However, in practice the two layers do not stay cleanly separated. For example, in the verification of the Knuth-Morris-Pratt (KMP) algorithm, the implementation correctness proof often re-establishes algorithm properties that have already been proved, as the concrete implementation relies on invariants that the traditional two-layer method provides no mechanism to transfer. This makes it difficult to clearly separate the concerns of algorithm correctness and implementation correctness. In this pearl, we show how a clean separation can be achieved within the two-layer method by combining two simple ideas: expressing implementation correctness as a relational Hoare quadruple, and introducing assertion annotations into the abstract program to capture key invariants. Properties established in the algorithm proof are thereby transferred directly to the implementation proof, eliminating the need to re-prove them. We demonstrate the effectiveness of this approach through non-trivial case studies, including the Knuth-Morris-Pratt pattern-matching algorithm and the depth-first search algorithm, showing that it leads to simpler proofs and a more modular verification process.