Coexponential Exploration in the Clef Programming Language

Houston Haynes

Home/Archive/arXiv

arXiv · 2610.12911

Coexponential Exploration in the Clef Programming Language

Houston Haynes

View original source ↗Read source document ↗Export metadata ↓

Abstract

Clef was created as a concurrent programming language whose compiler tracks state ownership, waiting computations and request dependencies. We develop a coexponential account of stateful services and their client pools within this design. Delimited continuations retain the computation and resources needed to complete each interaction. These structures give our compiler premises for verifying service composition and preserving it through native lowering to multiple hardware targets. We connect finite actor state transitions to the initial, service and final rules of a coexponential server. A separate operational account relates actor dispatch to single-use continuation frames. We prove state-ownership and reply preservation for that translation, give a finite communication-summary analysis, and circular-wait exclusion from the conditions needed. A further result identifies when changing service order preserves both state and replies. Our Program Semantic Graph retains these facts through compilation. We are researching reusable proofs to confirm the ownership and communication interfaces, while our BAREWire implementation connects message meaning to its unboxed representation across respective endpoints. A distributed worker example preserves request identity across suspension, reordered replies and boundary conversion. Urschel's elimination-growth bounds supply quantitative premises for a solver service, whose accuracy and failure budget compose with the protocol contract. The design we envision connects automatic structural analysis, reusable proof terms and native realization. Protocols determine the admissible interactions, continuations expose their storage requirements, and retained dependencies support differential compilation. Developers can express ordinary stateful services while the compiler carries the conditions for their correct composition across execution targets.

Explore related subjects

cs.PL cs.DC cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Houston Haynes. 2026-10-09. Coexponential Exploration in the Clef Programming Language. https://arxiv.org/abs/2610.12911

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

FlowBook: Enforcing Reproducibility in Computational Notebooks

Computational notebooks interleave code cells with their outputs and let users edit and execute cells in arbitrary order. This flexibility supports interactive exploration, but it also allows outputs to become inconsistent with the notebook's current code and data. Such inconsistencies can lead users to draw invalid scientific conclusions. We argue that notebooks should always be output consistent: every output should match what a top-to-bottom execution of the current code would produce. Forcing a top-to-bottom execution after each edit would guarantee this, but at prohibitive cost: such an execution can take minutes to hours. We present FlowBook, a dynamic analysis for Python notebooks that enforces output consistency without giving up out-of-order execution. FlowBook does this by enforcing a stronger property, rerun consistency: no location read by a cell may be written by any cell below it. Rerun consistency guarantees that rerunning a cell later, in any order, reproduces its current output. FlowBook tracks each cell's read and write sets at cell boundaries, blocks updates that would violate rerun consistency, and marks as stale any cell whose inputs may have changed. We prove that a notebook with no stale cells is both rerun and output consistent. Users remain free to execute cells in arbitrary order; the only restriction is that recorded outputs may not silently depend on the order in which cells were executed. Across 61 real-world notebooks, FlowBook flagged 203 rerun-inconsistent cells. Rerunning 62% led to output inconsistencies. A further 21% change notebook state with no visible output, which can affect the results of later edits and reruns; only 5% are false positives of FlowBook's conservative analysis. FlowBook's AI repair agent repaired all 203 cells with local edits and no human intervention. FlowBook's median overhead is only 26 ms per cell execution.

cs.PL↗

arXiv2026

From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware

Enforcing invariants in safety-critical firmware is increasingly urgent as generated code becomes widespread, but standard extraction targets for proof assistants require runtimes too large for many embedded devices. We present a pipeline for running formally verified Rocq firmware logic on Cortex-M microcontrollers. The pipeline extracts Gallina to Scheme, compiles it with Encore!, a bare-metal Continuation-Passing Style (CPS) bytecode virtual machine, and embeds the result in no_std Rust firmware. We structure applications as pure state-transition functions, so the business logic is proved in Rocq while the event/effect boundary, host callbacks, compiler, and VM remain explicit trusted components: no proof yet relates bytecode execution to Gallina semantics. On eight firmware workloads, from APDU parsing to a credential store, Encore! runs unmodified Rocq-extracted code within the 50 KiB RAM budget of ST33-class targets on every input size, where CertiRocq's generated code runs out of memory on the larger ones, at the price of up to 10 times more executed instructions than CertiRocq; a transaction-signing application is validated on physical Ledger Flex hardware.

cs.PL↗

arXiv2026

Compositional Information Geometry of Probabilistic Programs

We study the compositional, intensional information geometry of probabilistic programs. For a first-order probabilistic programming language with finite random variables, we construct a contravariant lax monoidal functor that, for a program of type $X \to Y$, pulls back a (degenerate) Riemannian metric on $Y$ to $X$. It specialises to the Fisher metric in the case of standard statistical models and to ordinary pullback in the case of deterministic programs. We further justify this construction in two ways. First, we show that this functor arises as a pullback of geometry from a universal space of programs over a type $Y$ with a fixed trace space. Second, we show that it is a special case of a more general pullback construction over weighted measures. Our compositional geometry depends on the presentation of the program, and we study how it relates to the (non-compositional) geometry of the realised measures by establishing a three-level inequality relating our score-velocity metric for the program, the program's corresponding output-conditioned metric, and the standard Wasserstein-Fisher-Rao metric of the realised family. Finally, we show how the theory can be extended to accommodate continuous random variables using diffeological quasi-Borel spaces. We also discuss several concrete directions for future work.

cs.PL↗