Proc. ACM Program. Lang., vol. 10, issue ICFP: "On Recursion in Graded Modal ..."
On Recursion in Graded Modal Type Theory
Oskar Eriksson, Andreas Abel, and Nils Anders Danielsson
(University of Gothenburg and Chalmers University of Technology, Gothenburg, Sweden)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p27-p (type: Full Paper) doi:10.1145/3828677
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Misquoted No More: Securely ..."
Misquoted No More: Securely Extracting F* Programs with IO
Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Cătălin Hrițcu, Exequiel Rivas, and Théo Winterhalter
(MPI-SP, Germany; MPI-SWS, Germany; University of Tartu, Estonia; Tallinn University of Technology, Estonia; Inria, France; LMF, France)
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 lambda-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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p64-p (type: Full Paper) doi:10.1145/3828689
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Package Managers à la Carte: ..."
Package Managers à la Carte: A Formal Model of Dependency Resolution
Ryan T. Gibb, Patrick Ferris, David Allsopp, Thomas Gazagnaire, and Anil Madhavapeddy
(University of Cambridge, UK; Jane Street, UK; Tarides, France)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p94-p (type: Full Paper) doi:10.1145/3828699
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Misquoted No More: Securely ..."
Misquoted No More: Securely Extracting F* Programs with IO
Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Cătălin Hrițcu, Exequiel Rivas, and Théo Winterhalter
(MPI-SP, Germany; MPI-SWS, Germany; University of Tartu, Estonia; Tallinn University of Technology, Estonia; Inria, France; LMF, France)
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 lambda-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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p64-p (type: Full Paper) doi:10.1145/3828689
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Safety First: How to Safely ..."
Safety First: How to Safely Disregard Unsafe Behaviour in Compiler Calculations
Patrick Bahr
(IT University of Copenhagen, Denmark)
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.
Publisher's Version
Article: icfp26main-p43-p (type: Full Paper) doi:10.1145/3828683
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Inlining as a Space Optimization: ..."
Inlining as a Space Optimization: A Simple Time- and Space-Invariant Implementation of the Weak Lambda-Calculus
Thibaut Balabonski
(Université Paris-Saclay - CNRS - LMF, France)
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.
Publisher's Version
ACM SIGPLAN Distinguished Paper Award
Article: icfp26main-p107-p (type: Full Paper) doi:10.1145/3828705
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Set-Theoretic Types for Erlang ..."
Set-Theoretic Types for Erlang in Practice (Experience Report)
Albert Schimpf and Annette Bieniusa
(University of Kaiserslautern-Landau, Germany)
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.
Publisher's Version
Article: icfp26main-p114-p (type: Full Paper (14 pages + Appendix + References)) doi:10.1145/3828708
Proc. ACM Program. Lang., vol. 10, issue ICFP: "LoCalMem: Type-Directed Adaptive ..."
LoCalMem: Type-Directed Adaptive Serialization for Location- and Content-Addressable Memory
Michael Rainey, Michael H. Borkowski, Michael Vollmer, Chaitanya S. Koparkar, Mikah Kainen, and Vidush Singhal
(Carnegie Mellon University, USA; Purdue University, USA; University of Kent, UK; MathWorks, USA)
Functional programming languages support non-destructive updates via structural sharing, creating a fundamental 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: icfp26main-p60-p (type: Full Paper) doi:10.1145/3828688
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Compositional Neural-Cyber-Physical ..."
Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice
Matthew L. Daggitt, Ekaterina Komendantskaya, Alistair Sirman, Alessandro Bruni, Samuel Teuber, Josh Smart, and Grant Passmore
(University of Western Australia, Australia; Heriot-Watt University, UK; University of Southampton, UK; IT University of Copenhagen, Denmark; KIT, Germany; Imandra, USA)
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 a coherent and consistent way, whilst preserving deployability of the resulting model. 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p34-p (type: Full Paper) doi:10.1145/3828680
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Assertions for Free: Transferring ..."
Assertions for Free: Transferring Invariants from Algorithm to Implementation Proofs (Functional Pearl)
Shushu Wu, Chengxi Yang, Xiwei Wu, and Qinxiang Cao
(Shanghai Jiao Tong University, China)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p76-p (type: Full Paper) doi:10.1145/3828694
Proc. ACM Program. Lang., vol. 10, issue ICFP: "When Types Intersect and Effects ..."
When Types Intersect and Effects Get Handled
Stefano Catozi, Ugo Dal Lago, and Taro Sekiyama
(University Sorbonne Paris Nord, France; University of Bologna, Italy; National Institute of Informatics, Japan)
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.
Publisher's Version
Article: icfp26main-p111-p (type: Full Paper) doi:10.1145/3828707
Proc. ACM Program. Lang., vol. 10, issue ICFP: "A Catenable, Splittable, Transient ..."
A Catenable, Splittable, Transient Sequence Data Structure
Arthur Charguéraud and François Pottier
(Inria, France; Université de Strasbourg, France; CNRS, France)
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(KlogK n), pushing and popping at either end with complexity O(KlogK n), and splitting and concatenation with complexity O(KlogK n+logK2 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.
Publisher's Version
ACM SIGPLAN Distinguished Paper Award
Article: icfp26main-p109-p (type: Full Paper) doi:10.1145/3828706
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Compositional Generator Equivalence ..."
Compositional Generator Equivalence
Anthony Vandikas, Kiarash Sotoudeh, and Marsha Chechik
(University of Toronto, Canada)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p81-p (type: Full Paper) doi:10.1145/3828695
Proc. ACM Program. Lang., vol. 10, issue ICFP: "QuickChecking Convergence ..."
QuickChecking Convergence of Rewriting Systems (Functional Pearl)
Koen Claessen
(Chalmers University of Technology and University of Gothenburg, Sweden)
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.
Publisher's Version
Article: icfp26main-p29-p (type: Full Paper) doi:10.1145/3828678
Proc. ACM Program. Lang., vol. 10, issue ICFP: "LazyHMC: Hamiltonian Monte ..."
LazyHMC: Hamiltonian Monte Carlo Simulation for Lazy, Infinite Dimensional Probabilistic Programs
Maria-Nicoleta Crăciun, C.-H. Luke Ong, Tom Schrijvers, and Sam Staton
(University of Oxford, UK; Nanyang Technological University, Singapore; KU Leuven, Belgium)
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.
Publisher's Version
Article: icfp26main-p82-p (type: Full Paper) doi:10.1145/3828696
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Compositional Neural-Cyber-Physical ..."
Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice
Matthew L. Daggitt, Ekaterina Komendantskaya, Alistair Sirman, Alessandro Bruni, Samuel Teuber, Josh Smart, and Grant Passmore
(University of Western Australia, Australia; Heriot-Watt University, UK; University of Southampton, UK; IT University of Copenhagen, Denmark; KIT, Germany; Imandra, USA)
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 a coherent and consistent way, whilst preserving deployability of the resulting model. 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p34-p (type: Full Paper) doi:10.1145/3828680
Proc. ACM Program. Lang., vol. 10, issue ICFP: "When Types Intersect and Effects ..."
When Types Intersect and Effects Get Handled
Stefano Catozi, Ugo Dal Lago, and Taro Sekiyama
(University Sorbonne Paris Nord, France; University of Bologna, Italy; National Institute of Informatics, Japan)
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.
Publisher's Version
Article: icfp26main-p111-p (type: Full Paper) doi:10.1145/3828707
Proc. ACM Program. Lang., vol. 10, issue ICFP: "On Recursion in Graded Modal ..."
On Recursion in Graded Modal Type Theory
Oskar Eriksson, Andreas Abel, and Nils Anders Danielsson
(University of Gothenburg and Chalmers University of Technology, Gothenburg, Sweden)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p27-p (type: Full Paper) doi:10.1145/3828677
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Mode Crossing ..."
Mode Crossing
Benjamin Peters, Jules Jacobs, Diana Kalinichenko, Liam Stevenson, Aspen Smith, Derek Dreyer, and Richard A. Eisenberg
(MPI-SWS, Germany; Jane Street, USA)
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, modal 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. To support mode crossing in the presence of abstract type specifications, 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 recursive and 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 the OxCaml compiler and deployed in a large industrial codebase, demonstrating practical usability.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p36-p (type: Full Paper) doi:10.1145/3828681
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Proofs Promptly: Proof-Oriented ..."
Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report)
Eleftherios Ioannidis, Nikhil Swamy, Gabriel Ebner, Matthai Philipose, and Tahina Ramananandro
(Microsoft Research, USA)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: icfp26main-p118-p (type: Full Paper (14 pages + Appendix + References)) doi:10.1145/3828709
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Mode Crossing ..."
Mode Crossing
Benjamin Peters, Jules Jacobs, Diana Kalinichenko, Liam Stevenson, Aspen Smith, Derek Dreyer, and Richard A. Eisenberg
(MPI-SWS, Germany; Jane Street, USA)
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, modal 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. To support mode crossing in the presence of abstract type specifications, 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 recursive and 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 the OxCaml compiler and deployed in a large industrial codebase, demonstrating practical usability.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p36-p (type: Full Paper) doi:10.1145/3828681
Proc. ACM Program. Lang., vol. 10, issue ICFP: "On Recursion in Graded Modal ..."
On Recursion in Graded Modal Type Theory
Oskar Eriksson, Andreas Abel, and Nils Anders Danielsson
(University of Gothenburg and Chalmers University of Technology, Gothenburg, Sweden)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p27-p (type: Full Paper) doi:10.1145/3828677
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Confluence Techniques for ..."
Confluence Techniques for Dependent Type Theory with Typed Conversion
Thiago Felicissimo and Théo Winterhalter
(Inria Rennes, France; Inria, France; LMF, France)
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 this work, we show how to 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 eta) and universes, but also some inductive types (Nat and sums), dependent pairs (without eta), definitional proof irrelevance and a lift type (with eta), 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p71-p (type: Full Paper) doi:10.1145/3828691
Proc. ACM Program. Lang., vol. 10, issue ICFP: "First-Class Constrained Types: ..."
First-Class Constrained Types: Elaboration, Type Inference, Approximation, and a Characterization of Termination
Chun Kit Lam, Florent Ferrari, and Lionel Parreaux
(Hong Kong University of Science and Technology, Hong Kong; ENS de Lyon, France)
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 semi-algorithm, called FCCTI, which makes no approximations and can thus be seen as an idealized “ground truth” of type inference. We show that FCCTI indirectly simulates term reduction, shedding some light on the difficulty of bounded polymorphic type inference. Finally, we extend FCCTI 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
ACM SIGPLAN Distinguished Paper Award
Article: icfp26main-p97-p (type: Full Paper) doi:10.1145/3828701
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Package Managers à la Carte: ..."
Package Managers à la Carte: A Formal Model of Dependency Resolution
Ryan T. Gibb, Patrick Ferris, David Allsopp, Thomas Gazagnaire, and Anil Madhavapeddy
(University of Cambridge, UK; Jane Street, UK; Tarides, France)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p94-p (type: Full Paper) doi:10.1145/3828699
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Animated Pictures for Slide ..."
Animated Pictures for Slide Presentations: From the Shallows to the Depths of a Domain-Specific Language (Functional Pearl)
Oliver Flatt, Robert Bruce Findler, and Matthew Flatt
(University of Washington, USA; Northwestern University, USA; University of Utah, USA)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p73-p (type: Full Paper) doi:10.1145/3828692
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Animated Pictures for Slide ..."
Animated Pictures for Slide Presentations: From the Shallows to the Depths of a Domain-Specific Language (Functional Pearl)
Oliver Flatt, Robert Bruce Findler, and Matthew Flatt
(University of Washington, USA; Northwestern University, USA; University of Utah, USA)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p73-p (type: Full Paper) doi:10.1145/3828692
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Animated Pictures for Slide ..."
Animated Pictures for Slide Presentations: From the Shallows to the Depths of a Domain-Specific Language (Functional Pearl)
Oliver Flatt, Robert Bruce Findler, and Matthew Flatt
(University of Washington, USA; Northwestern University, USA; University of Utah, USA)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p73-p (type: Full Paper) doi:10.1145/3828692
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Programmable Property-Based ..."
Programmable Property-Based Testing
Alperen Keles, Justine Frank, Ceren Mert, Harrison Goldstein, and Leonidas Lampropoulos
(University of Maryland, College Park, USA; SUNY Buffalo, USA)
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 rapidly prototyping a variety of property runners, highlighting domain-specific testing improvements that can be unlocked by more programmable testing.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
ACM SIGPLAN Distinguished Paper Award
Article: icfp26main-p56-p (type: Full Paper) doi:10.1145/3828685
Proc. ACM Program. Lang., vol. 10, issue ICFP: "An Equational and Graphical ..."
An Equational and Graphical Fixed-Point Calculus (Functional Pearl)
Gustavo de Mendonça Freire, Hugo Musso Gualandi, Hugo Nobrega, and Joao Paixao
(Federal University of Rio de Janeiro, Brazil)
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.
Publisher's Version
Article: icfp26main-p12-p (type: Full Paper) doi:10.1145/3828673
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Package Managers à la Carte: ..."
Package Managers à la Carte: A Formal Model of Dependency Resolution
Ryan T. Gibb, Patrick Ferris, David Allsopp, Thomas Gazagnaire, and Anil Madhavapeddy
(University of Cambridge, UK; Jane Street, UK; Tarides, France)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p94-p (type: Full Paper) doi:10.1145/3828699
Proc. ACM Program. Lang., vol. 10, issue ICFP: "RunbookFX: Type- and Effect-Safe ..."
RunbookFX: Type- and Effect-Safe LLM Synthesis for Executable Incident Diagnosis and Mitigation
Yifan Xiao, Shijie Li, and Yuhao Ge
(Peking University, China; China Southern Power Grid Company Limited, China)
Large language models are increasingly deployed as autonomous agents for cloud incident response, yet their direct use admits hallucinated diagnoses, unauthorized actions, irreversible changes, and unauditable decision trails. We present RunbookFX, a typed functional domain-specific language that elevates incident response from natural-language suggestions to executable programs whose safety is established statically. The key insight is that incident-response safety decomposes into three interacting dimensions: risk severity, exercised capabilities, and rollback resource availability. RunbookFX formalizes this decomposition as a product effect algebra Risk × K × ℕ whose four cross-component interaction axioms yield domain-specific safety theorems unexpressible in flat effect frameworks; a strong handler parametricity result then transfers these guarantees from a replay handler to any bisimilar live handler, bridging offline verification and production deployment. An LLM proposes candidate programs that a CEGIS-style verifier filters by static type checking and dynamic contract replay. A ∼2,200-line Coq development discharges the product effect algebra, its composition-preservation property, and four core safety theorems: Effect WF Preservation, Progress, single-step No Unauthorized Action, and Rollback Linearity. Of the 27 supporting obligations in the substitution and multi-step layers, 18 now close with Qed—including all Canonical Forms, all effect-operation Inversion lemmas, Value Typing, de Bruijn weakening, and the typing-respecting reduction cases for observe, act, rollback, and the affirmative guard; the remaining nine trace back to the de Bruijn substitution lemma, whose proof skeleton follows Pierce et al. [2019]. Evaluated on RCAEval for root cause analysis and ITBench for end-to-end mitigation, RunbookFX achieves 64% Top-1 RCA accuracy against 53% for the best LLM baseline and 38% mitigation success at 3.3× the official ITBench agent, with zero safety violations and 100% rollback coverage by construction.
Publisher's Version
Article: icfp26main-p21-p (type: Full Paper) doi:10.1145/3828675
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Demand-on-Demand Control-Flow ..."
Demand-on-Demand Control-Flow Analysis
Chahyun Kang and Kimball Germane
(Brigham Young University, USA)
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.
Publisher's Version
Article: icfp26main-p59-p (type: Full Paper) doi:10.1145/3828687
Proc. ACM Program. Lang., vol. 10, issue ICFP: "HMCFA: A Precise and Practical ..."
HMCFA: A Precise and Practical Big-Step Control Flow Analysis for Effect Handlers
Tim Whiting and Kimball Germane
(Brigham Young University, USA)
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. 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.
Publisher's Version
Article: icfp26main-p102-p (type: Full Paper) doi:10.1145/3828703
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Package Managers à la Carte: ..."
Package Managers à la Carte: A Formal Model of Dependency Resolution
Ryan T. Gibb, Patrick Ferris, David Allsopp, Thomas Gazagnaire, and Anil Madhavapeddy
(University of Cambridge, UK; Jane Street, UK; Tarides, France)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p94-p (type: Full Paper) doi:10.1145/3828699
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Programmable Property-Based ..."
Programmable Property-Based Testing
Alperen Keles, Justine Frank, Ceren Mert, Harrison Goldstein, and Leonidas Lampropoulos
(University of Maryland, College Park, USA; SUNY Buffalo, USA)
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 rapidly prototyping a variety of property runners, highlighting domain-specific testing improvements that can be unlocked by more programmable testing.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
ACM SIGPLAN Distinguished Paper Award
Article: icfp26main-p56-p (type: Full Paper) doi:10.1145/3828685
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Towards a Higher-Order Bialgebraic ..."
Towards a Higher-Order Bialgebraic Denotational Semantics
Sergey Goncharov, Marco Peressotti, Stelios Tsampas, Henning Urbat, and Stefano Volpe
(University of Birmingham, UK; University of Southern Denmark, Denmark; Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany)
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.
Publisher's Version
Article: icfp26main-p75-p (type: Full Paper) doi:10.1145/3828693
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Completeness of Iris-Based ..."
Completeness of Iris-Based Program Logics
Johannes Hostert, Zichen Zhang, Puming Liu, Simon Oddershede Gregersen, Ralf Jung, and Joseph Tassarotti
(ETH Zurich, Switzerland; New York University, USA; NYU Shanghai, China; CISPA Helmholtz Center for Information Security, Germany)
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 had 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 the Rocq prover.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p39-p (type: Full Paper) doi:10.1145/3828682
Proc. ACM Program. Lang., vol. 10, issue ICFP: "An Equational and Graphical ..."
An Equational and Graphical Fixed-Point Calculus (Functional Pearl)
Gustavo de Mendonça Freire, Hugo Musso Gualandi, Hugo Nobrega, and Joao Paixao
(Federal University of Rio de Janeiro, Brazil)
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.
Publisher's Version
Article: icfp26main-p12-p (type: Full Paper) doi:10.1145/3828673
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Citrus: Algebraic Reasoning ..."
Citrus: Algebraic Reasoning about Superconductor Electronics
Harlan Kringen, Timothy Sherwood, and Ben Hardekopf
(University of California at Santa Barbara, USA)
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.
Publisher's Version
Published Artifact
Artifacts Available
Article: icfp26main-p68-p (type: Full Paper) doi:10.1145/3828690
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Tail Modulo Async-Await ..."
Tail Modulo Async-Await
Emma Nardino, Ludovic Henrio, Gabriel Radanne, and Yannick Zakowski
(ENS Lyon - Univ Lyon - UCBL - CNRS - Inria - LIP, France; CNRS - Univ Lyon - ENS Lyon - UCBL - Inria - LIP, France; Inria - Univ Lyon - ENS Lyon - UCBL - CNRS - LIP, France; Inria, France)
This article extends tail-call optimisation by applying it to asynchronous calls. We first introduce TMA, a novel code transformation for asynchronous tail recursive functions that prevents the creation of unnecessary tasks. We then show how to combine TMA with the existing TMC 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
Publisher's Version
Published Artifact
Artifacts Available
Article: icfp26main-p52-p (type: Full Paper) doi:10.1145/3828684
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Programming Backpropagation ..."
Programming Backpropagation with Reverse Handlers for Arrows
Takahiro Sanada, Keisuke Hoshino, Kenshin Hirai, and Shin-ya Katsumata
(Fukui Prefectural University, Japan; Kyoto University, Japan; Kyoto Sangyo University, Japan)
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.
Publisher's Version
Article: icfp26main-p104-p (type: Full Paper) doi:10.1145/3828704
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Programming Backpropagation ..."
Programming Backpropagation with Reverse Handlers for Arrows
Takahiro Sanada, Keisuke Hoshino, Kenshin Hirai, and Shin-ya Katsumata
(Fukui Prefectural University, Japan; Kyoto University, Japan; Kyoto Sangyo University, Japan)
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.
Publisher's Version
Article: icfp26main-p104-p (type: Full Paper) doi:10.1145/3828704
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Completeness of Iris-Based ..."
Completeness of Iris-Based Program Logics
Johannes Hostert, Zichen Zhang, Puming Liu, Simon Oddershede Gregersen, Ralf Jung, and Joseph Tassarotti
(ETH Zurich, Switzerland; New York University, USA; NYU Shanghai, China; CISPA Helmholtz Center for Information Security, Germany)
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 had 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 the Rocq prover.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p39-p (type: Full Paper) doi:10.1145/3828682
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Misquoted No More: Securely ..."
Misquoted No More: Securely Extracting F* Programs with IO
Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Cătălin Hrițcu, Exequiel Rivas, and Théo Winterhalter
(MPI-SP, Germany; MPI-SWS, Germany; University of Tartu, Estonia; Tallinn University of Technology, Estonia; Inria, France; LMF, France)
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 lambda-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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p64-p (type: Full Paper) doi:10.1145/3828689
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Adequacy for Predicate Transformer ..."
Adequacy for Predicate Transformer Semantics
Kazuki Watanabe, Mirai Ikebuchi, and Mayuko Kori
(National Institute of Informatics, Japan; Kyoto University, Japan)
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.
Publisher's Version
Article: icfp26main-p18-p (type: Full Paper) doi:10.1145/3828674
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Proofs Promptly: Proof-Oriented ..."
Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report)
Eleftherios Ioannidis, Nikhil Swamy, Gabriel Ebner, Matthai Philipose, and Tahina Ramananandro
(Microsoft Research, USA)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: icfp26main-p118-p (type: Full Paper (14 pages + Appendix + References)) doi:10.1145/3828709
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Mode Crossing ..."
Mode Crossing
Benjamin Peters, Jules Jacobs, Diana Kalinichenko, Liam Stevenson, Aspen Smith, Derek Dreyer, and Richard A. Eisenberg
(MPI-SWS, Germany; Jane Street, USA)
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, modal 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. To support mode crossing in the presence of abstract type specifications, 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 recursive and 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 the OxCaml compiler and deployed in a large industrial codebase, demonstrating practical usability.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p36-p (type: Full Paper) doi:10.1145/3828681
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Completeness of Iris-Based ..."
Completeness of Iris-Based Program Logics
Johannes Hostert, Zichen Zhang, Puming Liu, Simon Oddershede Gregersen, Ralf Jung, and Joseph Tassarotti
(ETH Zurich, Switzerland; New York University, USA; NYU Shanghai, China; CISPA Helmholtz Center for Information Security, Germany)
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 had 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 the Rocq prover.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p39-p (type: Full Paper) doi:10.1145/3828682
Proc. ACM Program. Lang., vol. 10, issue ICFP: "LoCalMem: Type-Directed Adaptive ..."
LoCalMem: Type-Directed Adaptive Serialization for Location- and Content-Addressable Memory
Michael Rainey, Michael H. Borkowski, Michael Vollmer, Chaitanya S. Koparkar, Mikah Kainen, and Vidush Singhal
(Carnegie Mellon University, USA; Purdue University, USA; University of Kent, UK; MathWorks, USA)
Functional programming languages support non-destructive updates via structural sharing, creating a fundamental 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: icfp26main-p60-p (type: Full Paper) doi:10.1145/3828688
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Mode Crossing ..."
Mode Crossing
Benjamin Peters, Jules Jacobs, Diana Kalinichenko, Liam Stevenson, Aspen Smith, Derek Dreyer, and Richard A. Eisenberg
(MPI-SWS, Germany; Jane Street, USA)
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, modal 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. To support mode crossing in the presence of abstract type specifications, 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 recursive and 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 the OxCaml compiler and deployed in a large industrial codebase, demonstrating practical usability.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p36-p (type: Full Paper) doi:10.1145/3828681
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Demand-on-Demand Control-Flow ..."
Demand-on-Demand Control-Flow Analysis
Chahyun Kang and Kimball Germane
(Brigham Young University, USA)
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.
Publisher's Version
Article: icfp26main-p59-p (type: Full Paper) doi:10.1145/3828687
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Programming Backpropagation ..."
Programming Backpropagation with Reverse Handlers for Arrows
Takahiro Sanada, Keisuke Hoshino, Kenshin Hirai, and Shin-ya Katsumata
(Fukui Prefectural University, Japan; Kyoto University, Japan; Kyoto Sangyo University, Japan)
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.
Publisher's Version
Article: icfp26main-p104-p (type: Full Paper) doi:10.1145/3828704
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Bimodels and Biorthogonality ..."
Bimodels and Biorthogonality for Abstract Machines
April Tune and G. A. Kavvos
(University of Bristol, UK)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p57-p (type: Full Paper) doi:10.1145/3828686
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Programmable Property-Based ..."
Programmable Property-Based Testing
Alperen Keles, Justine Frank, Ceren Mert, Harrison Goldstein, and Leonidas Lampropoulos
(University of Maryland, College Park, USA; SUNY Buffalo, USA)
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 rapidly prototyping a variety of property runners, highlighting domain-specific testing improvements that can be unlocked by more programmable testing.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
ACM SIGPLAN Distinguished Paper Award
Article: icfp26main-p56-p (type: Full Paper) doi:10.1145/3828685
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Compositional Neural-Cyber-Physical ..."
Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice
Matthew L. Daggitt, Ekaterina Komendantskaya, Alistair Sirman, Alessandro Bruni, Samuel Teuber, Josh Smart, and Grant Passmore
(University of Western Australia, Australia; Heriot-Watt University, UK; University of Southampton, UK; IT University of Copenhagen, Denmark; KIT, Germany; Imandra, USA)
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 a coherent and consistent way, whilst preserving deployability of the resulting model. 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p34-p (type: Full Paper) doi:10.1145/3828680
Proc. ACM Program. Lang., vol. 10, issue ICFP: "LoCalMem: Type-Directed Adaptive ..."
LoCalMem: Type-Directed Adaptive Serialization for Location- and Content-Addressable Memory
Michael Rainey, Michael H. Borkowski, Michael Vollmer, Chaitanya S. Koparkar, Mikah Kainen, and Vidush Singhal
(Carnegie Mellon University, USA; Purdue University, USA; University of Kent, UK; MathWorks, USA)
Functional programming languages support non-destructive updates via structural sharing, creating a fundamental 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: icfp26main-p60-p (type: Full Paper) doi:10.1145/3828688
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Adequacy for Predicate Transformer ..."
Adequacy for Predicate Transformer Semantics
Kazuki Watanabe, Mirai Ikebuchi, and Mayuko Kori
(National Institute of Informatics, Japan; Kyoto University, Japan)
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.
Publisher's Version
Article: icfp26main-p18-p (type: Full Paper) doi:10.1145/3828674
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Citrus: Algebraic Reasoning ..."
Citrus: Algebraic Reasoning about Superconductor Electronics
Harlan Kringen, Timothy Sherwood, and Ben Hardekopf
(University of California at Santa Barbara, USA)
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.
Publisher's Version
Published Artifact
Artifacts Available
Article: icfp26main-p68-p (type: Full Paper) doi:10.1145/3828690
Proc. ACM Program. Lang., vol. 10, issue ICFP: "First-Class Constrained Types: ..."
First-Class Constrained Types: Elaboration, Type Inference, Approximation, and a Characterization of Termination
Chun Kit Lam, Florent Ferrari, and Lionel Parreaux
(Hong Kong University of Science and Technology, Hong Kong; ENS de Lyon, France)
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 semi-algorithm, called FCCTI, which makes no approximations and can thus be seen as an idealized “ground truth” of type inference. We show that FCCTI indirectly simulates term reduction, shedding some light on the difficulty of bounded polymorphic type inference. Finally, we extend FCCTI 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
ACM SIGPLAN Distinguished Paper Award
Article: icfp26main-p97-p (type: Full Paper) doi:10.1145/3828701
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Programmable Property-Based ..."
Programmable Property-Based Testing
Alperen Keles, Justine Frank, Ceren Mert, Harrison Goldstein, and Leonidas Lampropoulos
(University of Maryland, College Park, USA; SUNY Buffalo, USA)
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 rapidly prototyping a variety of property runners, highlighting domain-specific testing improvements that can be unlocked by more programmable testing.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
ACM SIGPLAN Distinguished Paper Award
Article: icfp26main-p56-p (type: Full Paper) doi:10.1145/3828685
Proc. ACM Program. Lang., vol. 10, issue ICFP: "RunbookFX: Type- and Effect-Safe ..."
RunbookFX: Type- and Effect-Safe LLM Synthesis for Executable Incident Diagnosis and Mitigation
Yifan Xiao, Shijie Li, and Yuhao Ge
(Peking University, China; China Southern Power Grid Company Limited, China)
Large language models are increasingly deployed as autonomous agents for cloud incident response, yet their direct use admits hallucinated diagnoses, unauthorized actions, irreversible changes, and unauditable decision trails. We present RunbookFX, a typed functional domain-specific language that elevates incident response from natural-language suggestions to executable programs whose safety is established statically. The key insight is that incident-response safety decomposes into three interacting dimensions: risk severity, exercised capabilities, and rollback resource availability. RunbookFX formalizes this decomposition as a product effect algebra Risk × K × ℕ whose four cross-component interaction axioms yield domain-specific safety theorems unexpressible in flat effect frameworks; a strong handler parametricity result then transfers these guarantees from a replay handler to any bisimilar live handler, bridging offline verification and production deployment. An LLM proposes candidate programs that a CEGIS-style verifier filters by static type checking and dynamic contract replay. A ∼2,200-line Coq development discharges the product effect algebra, its composition-preservation property, and four core safety theorems: Effect WF Preservation, Progress, single-step No Unauthorized Action, and Rollback Linearity. Of the 27 supporting obligations in the substitution and multi-step layers, 18 now close with Qed—including all Canonical Forms, all effect-operation Inversion lemmas, Value Typing, de Bruijn weakening, and the typing-respecting reduction cases for observe, act, rollback, and the affirmative guard; the remaining nine trace back to the de Bruijn substitution lemma, whose proof skeleton follows Pierce et al. [2019]. Evaluated on RCAEval for root cause analysis and ITBench for end-to-end mitigation, RunbookFX achieves 64% Top-1 RCA accuracy against 53% for the best LLM baseline and 38% mitigation success at 3.3× the official ITBench agent, with zero safety violations and 100% rollback coverage by construction.
Publisher's Version
Article: icfp26main-p21-p (type: Full Paper) doi:10.1145/3828675
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Imprecise Probabilistic Programming, ..."
Imprecise Probabilistic Programming, Precisely: Credal Sets via Graded Monads, BDDs, and Semiring-Parametric Inference (Functional Pearl)
Jack Liell-Cock and Sam Staton
(University of Oxford, UK)
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 Imp, 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.
Publisher's Version
Article: icfp26main-p87-p (type: Full Paper) doi:10.1145/3828698
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Same Coeffect, Different Base: ..."
Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types
Vilem Liepelt, Danielle Marshall, and Dominic Orchard
(University of Kent, UK; Royal Holloway University of London, UK; University of Cambridge, UK)
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.
Publisher's Version
Article: icfp26main-p85-p (type: Full Paper) doi:10.1145/3828697
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Completeness of Iris-Based ..."
Completeness of Iris-Based Program Logics
Johannes Hostert, Zichen Zhang, Puming Liu, Simon Oddershede Gregersen, Ralf Jung, and Joseph Tassarotti
(ETH Zurich, Switzerland; New York University, USA; NYU Shanghai, China; CISPA Helmholtz Center for Information Security, Germany)
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 had 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 the Rocq prover.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p39-p (type: Full Paper) doi:10.1145/3828682
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Package Managers à la Carte: ..."
Package Managers à la Carte: A Formal Model of Dependency Resolution
Ryan T. Gibb, Patrick Ferris, David Allsopp, Thomas Gazagnaire, and Anil Madhavapeddy
(University of Cambridge, UK; Jane Street, UK; Tarides, France)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p94-p (type: Full Paper) doi:10.1145/3828699
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Same Coeffect, Different Base: ..."
Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types
Vilem Liepelt, Danielle Marshall, and Dominic Orchard
(University of Kent, UK; Royal Holloway University of London, UK; University of Cambridge, UK)
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.
Publisher's Version
Article: icfp26main-p85-p (type: Full Paper) doi:10.1145/3828697
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Programmable Property-Based ..."
Programmable Property-Based Testing
Alperen Keles, Justine Frank, Ceren Mert, Harrison Goldstein, and Leonidas Lampropoulos
(University of Maryland, College Park, USA; SUNY Buffalo, USA)
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 rapidly prototyping a variety of property runners, highlighting domain-specific testing improvements that can be unlocked by more programmable testing.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
ACM SIGPLAN Distinguished Paper Award
Article: icfp26main-p56-p (type: Full Paper) doi:10.1145/3828685
Proc. ACM Program. Lang., vol. 10, issue ICFP: "A Separation Logic for Parallel ..."
A Separation Logic for Parallel Time Complexity with Work and Span Credits
Alexandre Moine, Sam Westrick, and Joseph Tassarotti
(New York University, USA)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p30-p (type: Full Paper) doi:10.1145/3828679
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Another Type Inference Algorithm ..."
Another Type Inference Algorithm for First-Class Implicit Polymorphism
J. Garrett Morris
(University of Iowa, USA)
We propose yet another approach to type inference with first-class implicit polymorphism, based on the interleaving of an Algorithm M-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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p99-p (type: Full Paper) doi:10.1145/3828702
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Unscanning by Möbius Inversion ..."
Unscanning by Möbius Inversion (Functional Pearl)
Keisuke Nakano
(Tohoku University, Japan)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p120-p (type: Full Paper) doi:10.1145/3828710
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Tail Modulo Async-Await ..."
Tail Modulo Async-Await
Emma Nardino, Ludovic Henrio, Gabriel Radanne, and Yannick Zakowski
(ENS Lyon - Univ Lyon - UCBL - CNRS - Inria - LIP, France; CNRS - Univ Lyon - ENS Lyon - UCBL - Inria - LIP, France; Inria - Univ Lyon - ENS Lyon - UCBL - CNRS - LIP, France; Inria, France)
This article extends tail-call optimisation by applying it to asynchronous calls. We first introduce TMA, a novel code transformation for asynchronous tail recursive functions that prevents the creation of unnecessary tasks. We then show how to combine TMA with the existing TMC 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
Publisher's Version
Published Artifact
Artifacts Available
Article: icfp26main-p52-p (type: Full Paper) doi:10.1145/3828684
Proc. ACM Program. Lang., vol. 10, issue ICFP: "An Equational and Graphical ..."
An Equational and Graphical Fixed-Point Calculus (Functional Pearl)
Gustavo de Mendonça Freire, Hugo Musso Gualandi, Hugo Nobrega, and Joao Paixao
(Federal University of Rio de Janeiro, Brazil)
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.
Publisher's Version
Article: icfp26main-p12-p (type: Full Paper) doi:10.1145/3828673
Proc. ACM Program. Lang., vol. 10, issue ICFP: "LazyHMC: Hamiltonian Monte ..."
LazyHMC: Hamiltonian Monte Carlo Simulation for Lazy, Infinite Dimensional Probabilistic Programs
Maria-Nicoleta Crăciun, C.-H. Luke Ong, Tom Schrijvers, and Sam Staton
(University of Oxford, UK; Nanyang Technological University, Singapore; KU Leuven, Belgium)
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.
Publisher's Version
Article: icfp26main-p82-p (type: Full Paper) doi:10.1145/3828696
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Same Coeffect, Different Base: ..."
Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types
Vilem Liepelt, Danielle Marshall, and Dominic Orchard
(University of Kent, UK; Royal Holloway University of London, UK; University of Cambridge, UK)
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.
Publisher's Version
Article: icfp26main-p85-p (type: Full Paper) doi:10.1145/3828697
Proc. ACM Program. Lang., vol. 10, issue ICFP: "An Equational and Graphical ..."
An Equational and Graphical Fixed-Point Calculus (Functional Pearl)
Gustavo de Mendonça Freire, Hugo Musso Gualandi, Hugo Nobrega, and Joao Paixao
(Federal University of Rio de Janeiro, Brazil)
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.
Publisher's Version
Article: icfp26main-p12-p (type: Full Paper) doi:10.1145/3828673
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Machine-Generated, Machine-Checked ..."
Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
Zoe Paraskevopoulou
(National Technical University of Athens, Greece)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p95-p (type: Full Paper (14 pages + Appendix + References)) doi:10.1145/3828700
Proc. ACM Program. Lang., vol. 10, issue ICFP: "First-Class Constrained Types: ..."
First-Class Constrained Types: Elaboration, Type Inference, Approximation, and a Characterization of Termination
Chun Kit Lam, Florent Ferrari, and Lionel Parreaux
(Hong Kong University of Science and Technology, Hong Kong; ENS de Lyon, France)
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 semi-algorithm, called FCCTI, which makes no approximations and can thus be seen as an idealized “ground truth” of type inference. We show that FCCTI indirectly simulates term reduction, shedding some light on the difficulty of bounded polymorphic type inference. Finally, we extend FCCTI 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
ACM SIGPLAN Distinguished Paper Award
Article: icfp26main-p97-p (type: Full Paper) doi:10.1145/3828701
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Compositional Neural-Cyber-Physical ..."
Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice
Matthew L. Daggitt, Ekaterina Komendantskaya, Alistair Sirman, Alessandro Bruni, Samuel Teuber, Josh Smart, and Grant Passmore
(University of Western Australia, Australia; Heriot-Watt University, UK; University of Southampton, UK; IT University of Copenhagen, Denmark; KIT, Germany; Imandra, USA)
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 a coherent and consistent way, whilst preserving deployability of the resulting model. 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p34-p (type: Full Paper) doi:10.1145/3828680
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Towards a Higher-Order Bialgebraic ..."
Towards a Higher-Order Bialgebraic Denotational Semantics
Sergey Goncharov, Marco Peressotti, Stelios Tsampas, Henning Urbat, and Stefano Volpe
(University of Birmingham, UK; University of Southern Denmark, Denmark; Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany)
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.
Publisher's Version
Article: icfp26main-p75-p (type: Full Paper) doi:10.1145/3828693
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Mode Crossing ..."
Mode Crossing
Benjamin Peters, Jules Jacobs, Diana Kalinichenko, Liam Stevenson, Aspen Smith, Derek Dreyer, and Richard A. Eisenberg
(MPI-SWS, Germany; Jane Street, USA)
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, modal 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. To support mode crossing in the presence of abstract type specifications, 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 recursive and 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 the OxCaml compiler and deployed in a large industrial codebase, demonstrating practical usability.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p36-p (type: Full Paper) doi:10.1145/3828681
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Proofs Promptly: Proof-Oriented ..."
Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report)
Eleftherios Ioannidis, Nikhil Swamy, Gabriel Ebner, Matthai Philipose, and Tahina Ramananandro
(Microsoft Research, USA)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: icfp26main-p118-p (type: Full Paper (14 pages + Appendix + References)) doi:10.1145/3828709
Proc. ACM Program. Lang., vol. 10, issue ICFP: "A Catenable, Splittable, Transient ..."
A Catenable, Splittable, Transient Sequence Data Structure
Arthur Charguéraud and François Pottier
(Inria, France; Université de Strasbourg, France; CNRS, France)
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(KlogK n), pushing and popping at either end with complexity O(KlogK n), and splitting and concatenation with complexity O(KlogK n+logK2 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.
Publisher's Version
ACM SIGPLAN Distinguished Paper Award
Article: icfp26main-p109-p (type: Full Paper) doi:10.1145/3828706
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Misquoted No More: Securely ..."
Misquoted No More: Securely Extracting F* Programs with IO
Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Cătălin Hrițcu, Exequiel Rivas, and Théo Winterhalter
(MPI-SP, Germany; MPI-SWS, Germany; University of Tartu, Estonia; Tallinn University of Technology, Estonia; Inria, France; LMF, France)
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 lambda-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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p64-p (type: Full Paper) doi:10.1145/3828689
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Tail Modulo Async-Await ..."
Tail Modulo Async-Await
Emma Nardino, Ludovic Henrio, Gabriel Radanne, and Yannick Zakowski
(ENS Lyon - Univ Lyon - UCBL - CNRS - Inria - LIP, France; CNRS - Univ Lyon - ENS Lyon - UCBL - Inria - LIP, France; Inria - Univ Lyon - ENS Lyon - UCBL - CNRS - LIP, France; Inria, France)
This article extends tail-call optimisation by applying it to asynchronous calls. We first introduce TMA, a novel code transformation for asynchronous tail recursive functions that prevents the creation of unnecessary tasks. We then show how to combine TMA with the existing TMC 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
Publisher's Version
Published Artifact
Artifacts Available
Article: icfp26main-p52-p (type: Full Paper) doi:10.1145/3828684
Proc. ACM Program. Lang., vol. 10, issue ICFP: "LoCalMem: Type-Directed Adaptive ..."
LoCalMem: Type-Directed Adaptive Serialization for Location- and Content-Addressable Memory
Michael Rainey, Michael H. Borkowski, Michael Vollmer, Chaitanya S. Koparkar, Mikah Kainen, and Vidush Singhal
(Carnegie Mellon University, USA; Purdue University, USA; University of Kent, UK; MathWorks, USA)
Functional programming languages support non-destructive updates via structural sharing, creating a fundamental 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: icfp26main-p60-p (type: Full Paper) doi:10.1145/3828688
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Proofs Promptly: Proof-Oriented ..."
Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report)
Eleftherios Ioannidis, Nikhil Swamy, Gabriel Ebner, Matthai Philipose, and Tahina Ramananandro
(Microsoft Research, USA)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: icfp26main-p118-p (type: Full Paper (14 pages + Appendix + References)) doi:10.1145/3828709
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Misquoted No More: Securely ..."
Misquoted No More: Securely Extracting F* Programs with IO
Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Cătălin Hrițcu, Exequiel Rivas, and Théo Winterhalter
(MPI-SP, Germany; MPI-SWS, Germany; University of Tartu, Estonia; Tallinn University of Technology, Estonia; Inria, France; LMF, France)
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 lambda-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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p64-p (type: Full Paper) doi:10.1145/3828689
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Programming Backpropagation ..."
Programming Backpropagation with Reverse Handlers for Arrows
Takahiro Sanada, Keisuke Hoshino, Kenshin Hirai, and Shin-ya Katsumata
(Fukui Prefectural University, Japan; Kyoto University, Japan; Kyoto Sangyo University, Japan)
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.
Publisher's Version
Article: icfp26main-p104-p (type: Full Paper) doi:10.1145/3828704
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Set-Theoretic Types for Erlang ..."
Set-Theoretic Types for Erlang in Practice (Experience Report)
Albert Schimpf and Annette Bieniusa
(University of Kaiserslautern-Landau, Germany)
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.
Publisher's Version
Article: icfp26main-p114-p (type: Full Paper (14 pages + Appendix + References)) doi:10.1145/3828708
Proc. ACM Program. Lang., vol. 10, issue ICFP: "LazyHMC: Hamiltonian Monte ..."
LazyHMC: Hamiltonian Monte Carlo Simulation for Lazy, Infinite Dimensional Probabilistic Programs
Maria-Nicoleta Crăciun, C.-H. Luke Ong, Tom Schrijvers, and Sam Staton
(University of Oxford, UK; Nanyang Technological University, Singapore; KU Leuven, Belgium)
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.
Publisher's Version
Article: icfp26main-p82-p (type: Full Paper) doi:10.1145/3828696
Proc. ACM Program. Lang., vol. 10, issue ICFP: "When Types Intersect and Effects ..."
When Types Intersect and Effects Get Handled
Stefano Catozi, Ugo Dal Lago, and Taro Sekiyama
(University Sorbonne Paris Nord, France; University of Bologna, Italy; National Institute of Informatics, Japan)
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.
Publisher's Version
Article: icfp26main-p111-p (type: Full Paper) doi:10.1145/3828707
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Editorial Message ..."
Editorial Message
Manuel Serrano
(Inria, France; Université Côte d’Azur, France)
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.
Publisher's Version
Article: icfp26editorial-fm001-p (type: Editorial) doi:10.1145/3833372
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Citrus: Algebraic Reasoning ..."
Citrus: Algebraic Reasoning about Superconductor Electronics
Harlan Kringen, Timothy Sherwood, and Ben Hardekopf
(University of California at Santa Barbara, USA)
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.
Publisher's Version
Published Artifact
Artifacts Available
Article: icfp26main-p68-p (type: Full Paper) doi:10.1145/3828690
Proc. ACM Program. Lang., vol. 10, issue ICFP: "LoCalMem: Type-Directed Adaptive ..."
LoCalMem: Type-Directed Adaptive Serialization for Location- and Content-Addressable Memory
Michael Rainey, Michael H. Borkowski, Michael Vollmer, Chaitanya S. Koparkar, Mikah Kainen, and Vidush Singhal
(Carnegie Mellon University, USA; Purdue University, USA; University of Kent, UK; MathWorks, USA)
Functional programming languages support non-destructive updates via structural sharing, creating a fundamental 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: icfp26main-p60-p (type: Full Paper) doi:10.1145/3828688
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Compositional Neural-Cyber-Physical ..."
Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice
Matthew L. Daggitt, Ekaterina Komendantskaya, Alistair Sirman, Alessandro Bruni, Samuel Teuber, Josh Smart, and Grant Passmore
(University of Western Australia, Australia; Heriot-Watt University, UK; University of Southampton, UK; IT University of Copenhagen, Denmark; KIT, Germany; Imandra, USA)
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 a coherent and consistent way, whilst preserving deployability of the resulting model. 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p34-p (type: Full Paper) doi:10.1145/3828680
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Compositional Neural-Cyber-Physical ..."
Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice
Matthew L. Daggitt, Ekaterina Komendantskaya, Alistair Sirman, Alessandro Bruni, Samuel Teuber, Josh Smart, and Grant Passmore
(University of Western Australia, Australia; Heriot-Watt University, UK; University of Southampton, UK; IT University of Copenhagen, Denmark; KIT, Germany; Imandra, USA)
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 a coherent and consistent way, whilst preserving deployability of the resulting model. 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p34-p (type: Full Paper) doi:10.1145/3828680
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Mode Crossing ..."
Mode Crossing
Benjamin Peters, Jules Jacobs, Diana Kalinichenko, Liam Stevenson, Aspen Smith, Derek Dreyer, and Richard A. Eisenberg
(MPI-SWS, Germany; Jane Street, USA)
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, modal 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. To support mode crossing in the presence of abstract type specifications, 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 recursive and 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 the OxCaml compiler and deployed in a large industrial codebase, demonstrating practical usability.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p36-p (type: Full Paper) doi:10.1145/3828681
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Compositional Generator Equivalence ..."
Compositional Generator Equivalence
Anthony Vandikas, Kiarash Sotoudeh, and Marsha Chechik
(University of Toronto, Canada)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p81-p (type: Full Paper) doi:10.1145/3828695
Proc. ACM Program. Lang., vol. 10, issue ICFP: "LazyHMC: Hamiltonian Monte ..."
LazyHMC: Hamiltonian Monte Carlo Simulation for Lazy, Infinite Dimensional Probabilistic Programs
Maria-Nicoleta Crăciun, C.-H. Luke Ong, Tom Schrijvers, and Sam Staton
(University of Oxford, UK; Nanyang Technological University, Singapore; KU Leuven, Belgium)
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.
Publisher's Version
Article: icfp26main-p82-p (type: Full Paper) doi:10.1145/3828696
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Imprecise Probabilistic Programming, ..."
Imprecise Probabilistic Programming, Precisely: Credal Sets via Graded Monads, BDDs, and Semiring-Parametric Inference (Functional Pearl)
Jack Liell-Cock and Sam Staton
(University of Oxford, UK)
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 Imp, 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.
Publisher's Version
Article: icfp26main-p87-p (type: Full Paper) doi:10.1145/3828698
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Mode Crossing ..."
Mode Crossing
Benjamin Peters, Jules Jacobs, Diana Kalinichenko, Liam Stevenson, Aspen Smith, Derek Dreyer, and Richard A. Eisenberg
(MPI-SWS, Germany; Jane Street, USA)
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, modal 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. To support mode crossing in the presence of abstract type specifications, 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 recursive and 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 the OxCaml compiler and deployed in a large industrial codebase, demonstrating practical usability.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p36-p (type: Full Paper) doi:10.1145/3828681
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Proofs Promptly: Proof-Oriented ..."
Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report)
Eleftherios Ioannidis, Nikhil Swamy, Gabriel Ebner, Matthai Philipose, and Tahina Ramananandro
(Microsoft Research, USA)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: icfp26main-p118-p (type: Full Paper (14 pages + Appendix + References)) doi:10.1145/3828709
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Let It Be Optimized: Building ..."
Let It Be Optimized: Building Multi-stage Evaluators with Let-Insertion and Optimizations in Small Pieces (Functional Pearl)
Guannan Wei, Jun Tan, and Dinghong Zhong
(Tufts University, USA; Independent, China)
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 beta-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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p23-p (type: Full Paper) doi:10.1145/3828676
Proc. ACM Program. Lang., vol. 10, issue ICFP: "A Separation Logic for Parallel ..."
A Separation Logic for Parallel Time Complexity with Work and Span Credits
Alexandre Moine, Sam Westrick, and Joseph Tassarotti
(New York University, USA)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p30-p (type: Full Paper) doi:10.1145/3828679
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Completeness of Iris-Based ..."
Completeness of Iris-Based Program Logics
Johannes Hostert, Zichen Zhang, Puming Liu, Simon Oddershede Gregersen, Ralf Jung, and Joseph Tassarotti
(ETH Zurich, Switzerland; New York University, USA; NYU Shanghai, China; CISPA Helmholtz Center for Information Security, Germany)
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 had 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 the Rocq prover.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p39-p (type: Full Paper) doi:10.1145/3828682
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Compositional Neural-Cyber-Physical ..."
Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice
Matthew L. Daggitt, Ekaterina Komendantskaya, Alistair Sirman, Alessandro Bruni, Samuel Teuber, Josh Smart, and Grant Passmore
(University of Western Australia, Australia; Heriot-Watt University, UK; University of Southampton, UK; IT University of Copenhagen, Denmark; KIT, Germany; Imandra, USA)
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 a coherent and consistent way, whilst preserving deployability of the resulting model. 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p34-p (type: Full Paper) doi:10.1145/3828680
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Towards a Higher-Order Bialgebraic ..."
Towards a Higher-Order Bialgebraic Denotational Semantics
Sergey Goncharov, Marco Peressotti, Stelios Tsampas, Henning Urbat, and Stefano Volpe
(University of Birmingham, UK; University of Southern Denmark, Denmark; Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany)
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.
Publisher's Version
Article: icfp26main-p75-p (type: Full Paper) doi:10.1145/3828693
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Bimodels and Biorthogonality ..."
Bimodels and Biorthogonality for Abstract Machines
April Tune and G. A. Kavvos
(University of Bristol, UK)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p57-p (type: Full Paper) doi:10.1145/3828686
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Towards a Higher-Order Bialgebraic ..."
Towards a Higher-Order Bialgebraic Denotational Semantics
Sergey Goncharov, Marco Peressotti, Stelios Tsampas, Henning Urbat, and Stefano Volpe
(University of Birmingham, UK; University of Southern Denmark, Denmark; Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany)
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.
Publisher's Version
Article: icfp26main-p75-p (type: Full Paper) doi:10.1145/3828693
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Compositional Generator Equivalence ..."
Compositional Generator Equivalence
Anthony Vandikas, Kiarash Sotoudeh, and Marsha Chechik
(University of Toronto, Canada)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p81-p (type: Full Paper) doi:10.1145/3828695
Proc. ACM Program. Lang., vol. 10, issue ICFP: "LoCalMem: Type-Directed Adaptive ..."
LoCalMem: Type-Directed Adaptive Serialization for Location- and Content-Addressable Memory
Michael Rainey, Michael H. Borkowski, Michael Vollmer, Chaitanya S. Koparkar, Mikah Kainen, and Vidush Singhal
(Carnegie Mellon University, USA; Purdue University, USA; University of Kent, UK; MathWorks, USA)
Functional programming languages support non-destructive updates via structural sharing, creating a fundamental 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: icfp26main-p60-p (type: Full Paper) doi:10.1145/3828688
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Towards a Higher-Order Bialgebraic ..."
Towards a Higher-Order Bialgebraic Denotational Semantics
Sergey Goncharov, Marco Peressotti, Stelios Tsampas, Henning Urbat, and Stefano Volpe
(University of Birmingham, UK; University of Southern Denmark, Denmark; Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany)
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.
Publisher's Version
Article: icfp26main-p75-p (type: Full Paper) doi:10.1145/3828693
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Adequacy for Predicate Transformer ..."
Adequacy for Predicate Transformer Semantics
Kazuki Watanabe, Mirai Ikebuchi, and Mayuko Kori
(National Institute of Informatics, Japan; Kyoto University, Japan)
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.
Publisher's Version
Article: icfp26main-p18-p (type: Full Paper) doi:10.1145/3828674
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Let It Be Optimized: Building ..."
Let It Be Optimized: Building Multi-stage Evaluators with Let-Insertion and Optimizations in Small Pieces (Functional Pearl)
Guannan Wei, Jun Tan, and Dinghong Zhong
(Tufts University, USA; Independent, China)
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 beta-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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p23-p (type: Full Paper) doi:10.1145/3828676
Proc. ACM Program. Lang., vol. 10, issue ICFP: "A Separation Logic for Parallel ..."
A Separation Logic for Parallel Time Complexity with Work and Span Credits
Alexandre Moine, Sam Westrick, and Joseph Tassarotti
(New York University, USA)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p30-p (type: Full Paper) doi:10.1145/3828679
Proc. ACM Program. Lang., vol. 10, issue ICFP: "HMCFA: A Precise and Practical ..."
HMCFA: A Precise and Practical Big-Step Control Flow Analysis for Effect Handlers
Tim Whiting and Kimball Germane
(Brigham Young University, USA)
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. 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.
Publisher's Version
Article: icfp26main-p102-p (type: Full Paper) doi:10.1145/3828703
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Misquoted No More: Securely ..."
Misquoted No More: Securely Extracting F* Programs with IO
Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Cătălin Hrițcu, Exequiel Rivas, and Théo Winterhalter
(MPI-SP, Germany; MPI-SWS, Germany; University of Tartu, Estonia; Tallinn University of Technology, Estonia; Inria, France; LMF, France)
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 lambda-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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p64-p (type: Full Paper) doi:10.1145/3828689
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Confluence Techniques for ..."
Confluence Techniques for Dependent Type Theory with Typed Conversion
Thiago Felicissimo and Théo Winterhalter
(Inria Rennes, France; Inria, France; LMF, France)
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 this work, we show how to 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 eta) and universes, but also some inductive types (Nat and sums), dependent pairs (without eta), definitional proof irrelevance and a lift type (with eta), 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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p71-p (type: Full Paper) doi:10.1145/3828691
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Assertions for Free: Transferring ..."
Assertions for Free: Transferring Invariants from Algorithm to Implementation Proofs (Functional Pearl)
Shushu Wu, Chengxi Yang, Xiwei Wu, and Qinxiang Cao
(Shanghai Jiao Tong University, China)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p76-p (type: Full Paper) doi:10.1145/3828694
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Assertions for Free: Transferring ..."
Assertions for Free: Transferring Invariants from Algorithm to Implementation Proofs (Functional Pearl)
Shushu Wu, Chengxi Yang, Xiwei Wu, and Qinxiang Cao
(Shanghai Jiao Tong University, China)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p76-p (type: Full Paper) doi:10.1145/3828694
Proc. ACM Program. Lang., vol. 10, issue ICFP: "RunbookFX: Type- and Effect-Safe ..."
RunbookFX: Type- and Effect-Safe LLM Synthesis for Executable Incident Diagnosis and Mitigation
Yifan Xiao, Shijie Li, and Yuhao Ge
(Peking University, China; China Southern Power Grid Company Limited, China)
Large language models are increasingly deployed as autonomous agents for cloud incident response, yet their direct use admits hallucinated diagnoses, unauthorized actions, irreversible changes, and unauditable decision trails. We present RunbookFX, a typed functional domain-specific language that elevates incident response from natural-language suggestions to executable programs whose safety is established statically. The key insight is that incident-response safety decomposes into three interacting dimensions: risk severity, exercised capabilities, and rollback resource availability. RunbookFX formalizes this decomposition as a product effect algebra Risk × K × ℕ whose four cross-component interaction axioms yield domain-specific safety theorems unexpressible in flat effect frameworks; a strong handler parametricity result then transfers these guarantees from a replay handler to any bisimilar live handler, bridging offline verification and production deployment. An LLM proposes candidate programs that a CEGIS-style verifier filters by static type checking and dynamic contract replay. A ∼2,200-line Coq development discharges the product effect algebra, its composition-preservation property, and four core safety theorems: Effect WF Preservation, Progress, single-step No Unauthorized Action, and Rollback Linearity. Of the 27 supporting obligations in the substitution and multi-step layers, 18 now close with Qed—including all Canonical Forms, all effect-operation Inversion lemmas, Value Typing, de Bruijn weakening, and the typing-respecting reduction cases for observe, act, rollback, and the affirmative guard; the remaining nine trace back to the de Bruijn substitution lemma, whose proof skeleton follows Pierce et al. [2019]. Evaluated on RCAEval for root cause analysis and ITBench for end-to-end mitigation, RunbookFX achieves 64% Top-1 RCA accuracy against 53% for the best LLM baseline and 38% mitigation success at 3.3× the official ITBench agent, with zero safety violations and 100% rollback coverage by construction.
Publisher's Version
Article: icfp26main-p21-p (type: Full Paper) doi:10.1145/3828675
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Assertions for Free: Transferring ..."
Assertions for Free: Transferring Invariants from Algorithm to Implementation Proofs (Functional Pearl)
Shushu Wu, Chengxi Yang, Xiwei Wu, and Qinxiang Cao
(Shanghai Jiao Tong University, China)
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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p76-p (type: Full Paper) doi:10.1145/3828694
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Tail Modulo Async-Await ..."
Tail Modulo Async-Await
Emma Nardino, Ludovic Henrio, Gabriel Radanne, and Yannick Zakowski
(ENS Lyon - Univ Lyon - UCBL - CNRS - Inria - LIP, France; CNRS - Univ Lyon - ENS Lyon - UCBL - Inria - LIP, France; Inria - Univ Lyon - ENS Lyon - UCBL - CNRS - LIP, France; Inria, France)
This article extends tail-call optimisation by applying it to asynchronous calls. We first introduce TMA, a novel code transformation for asynchronous tail recursive functions that prevents the creation of unnecessary tasks. We then show how to combine TMA with the existing TMC 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
Publisher's Version
Published Artifact
Artifacts Available
Article: icfp26main-p52-p (type: Full Paper) doi:10.1145/3828684
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Completeness of Iris-Based ..."
Completeness of Iris-Based Program Logics
Johannes Hostert, Zichen Zhang, Puming Liu, Simon Oddershede Gregersen, Ralf Jung, and Joseph Tassarotti
(ETH Zurich, Switzerland; New York University, USA; NYU Shanghai, China; CISPA Helmholtz Center for Information Security, Germany)
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 had 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 the Rocq prover.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p39-p (type: Full Paper) doi:10.1145/3828682
Proc. ACM Program. Lang., vol. 10, issue ICFP: "Let It Be Optimized: Building ..."
Let It Be Optimized: Building Multi-stage Evaluators with Let-Insertion and Optimizations in Small Pieces (Functional Pearl)
Guannan Wei, Jun Tan, and Dinghong Zhong
(Tufts University, USA; Independent, China)
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 beta-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.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: icfp26main-p23-p (type: Full Paper) doi:10.1145/3828676