Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.28525

What is a Good Projection?: Correctness and Separation Results of End-Point Projections

Jake Masters·Nobuko Yoshida
View original source ↗Read source document ↗Export metadata ↓

Abstract

\emph{Multiparty session types} (MPST) is a type discipline for ensuring distributed programs are implemented correctly \emph{by construction}. MPST starts by specifying a choreographic protocol as a \emph{global type} and \emph{projects} it onto each participant, generating \emph{local types} with a guarantee of type soundness and deadlock-freedom. A central issue of MPST is that its type soundness is fragile, as it must be proven each time with respect to a chosen projection algorithm under specific semantics with a specific program correctness goal. To overcome this problem, we propose general criteria for a \emph{good projection} -- a set of requirements for projection algorithms by which type soundness, deadlock-freedom and liveness of distributed programs are \emph{automatically} derived. Using the criteria, we prove that 8 distinct projections in the literature are good under both synchronous and asynchronous semantics, and that 4 are incorrect, failing type soundness. We extend the good projection criteria to mixed choice global types and asynchronous communication optimisations, proposing new ``good projection'' algorithms. We apply properties of good projections to prove \emph{separation} and \emph{expressiveness} results over the projection algorithms and MPST typing systems. Having a generalised typing system that is robust with respect to the good projection criteria, we provide an implementation with mixed choice global types that is \emph{modular} with respect to a chosen projection algorithm and desired program properties. Our separation results help programmers make informed trade-offs between complexity and expressiveness when choosing projection algorithms, and our theory ensures their chosen algorithms are correctly applied.

Explore related subjects

cs.PLcs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Jake Masters, Nobuko Yoshida. 2026-10-20. What is a Good Projection?: Correctness and Separation Results of End-Point Projections. https://arxiv.org/abs/2610.28525

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

KEEP EXPLORING

Related papers

arXiv2026

Operon: Incremental Construction of Ragged Data via Named Dimensions

Modern data processing workflows frequently encounter ragged data: multidimensional collections whose inner lengths vary and are revealed only at runtime. Ragged data is prevalent in domains throughout science and computing, yet existing workflow engines treat it as nested containers. This representation leaves shape semantics ambiguous, obscures task dependencies when upstream coordinates are not yet enumerated, and imposes coarse synchronization barriers that stall independent work across tasks. We argue that ragged data is fundamentally a flat function over a coordinate space, and that making this view explicit resolves all three difficulties at once. We realize this insight in Operon, a statically verifiable workflow engine built around a formalism of named dimensions with explicit dependency relations. Users declare pipelines in the Operon DSL by annotating data flow with dimension names, where the static checker verifies that every task does not include faulty iterations regardless of runtime lengths. At runtime, the system models in-progress arrays as partial functions over downward-closed coordinate domains, which provides a natural representation for partially-unknown data states, an exact notion of per-task indegree before all upstream coordinates are enumerated, and a sound basis for fault recovery without programmer intervention.

cs.PL↗
arXiv2026

Multiobjective Preexpectation Reasoning for Probabilistic Programs

Probabilistic programs with nondeterminism model planning problems in which a strategy typically resolves the nondeterminism to meet a specification. We study the multiobjective setting, meeting several specifications at once along a Pareto front, and provide a deductive, program-level account of strategy synthesis. Its core is a multiobjective preexpectation transformer mapping a tuple of postexpectations to the set of simultaneously achievable values, an element of the convex Hoare powerdomain. It conservatively extends weakest preexpectations and lifts standard loop rules. We develop rules to synthesize witnessing strategies as mixed determinizations that solve nondeterminism probabilistically. We prove the transformer and synthesis rules sound against an operational Markov decision process (MDP) semantics, without requiring a finite state space: our approach can be seen as a symbolic approach - at program level - for multiobjective optimization over infinite MDPs. We demonstrate our machinery using two case studies.

cs.PL↗
arXiv2026

Foundational Refinement Proofs for EVM Bytecode, at the Price of Tokens

Relating executable code to a high-level model of its behavior has been a central concern of programming-language research for decades. Formally verified compilers, translation validators and certifying compilers address this problem through different trade-offs between proof effort, automation, generality, and the size of the trusted base. Recently, large language models (LLMs) have begun to change the economics of formal verification. Agentic proof development is now capable of producing machine-checked proofs, sometimes unsupervised, at a scale and speed that were previously out of reach. We propose a verification architecture that takes advantage of this shift. An executable obtains a machine-checked proof that it behaves according to a high-level model, independently of the compiler that produced it. The proof is written by an LLM agent. We evaluate the feasibility of this architecture for the Ethereum Virtual Machine (EVM). We build EquiVM, a foundational framework in Lean comprising an executable EVM semantics and a formal specification language, Stele, that gives a high-level authoritative model of the bytecode's behavior, but commits to no source language or compilation toolchain. We state what it means for EVM bytecode to refine a Stele spec and we build a proof library to facilitate proof construction. We evaluate the capabilities of frontier LLMs to construct such proofs, as well as the cost of proof production and repair. Our results show that agents prove 35 real production contracts end to end, without modifying their source or bytecode, among them core contracts of Safe, Morpho, Compound and Uniswap protocols, with bytecode of size close to the maximum the EVM allows. Several proofs need only the initial prompt, the rest a handful of human inputs, and existing proofs are repaired in a fraction of the original time when the source or the compiler configuration changes.

cs.PL↗