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.
A transient data structure is a combination of an ephemeral data structure, a persistent data structure, and fast conversions between them. We present a transient sequence data structure that supports efficient read and write access at an arbitrary index with worst-case time complexity O ( K log K n ), pushing and popping at either end with complexity O ( K log K n ), and splitting and concatenation with complexity O ( K log K n +log K 2 n ), where K is a user-defined chunk size and n is the length of the sequence. We provide a detailed analysis of this data structure and show that, in many favorable scenarios, it performs much better than these pessimistic bounds might suggest. Furthermore, we describe its implementation, and provide a synthetic benchmark to evaluate the performance of push and pop . We believe that it is a good candidate for a one-size-fits-all, general-purpose sequence data structure.
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.
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
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 FCCT I , which makes no approximations and can thus be seen as an idealized “ground truth” of type inference. We show that FCCT I indirectly simulates term reduction, shedding some light on the difficulty of bounded polymorphic type inference. Finally, we extend FCCT I 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
