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

Jake Masters; Nobuko Yoshida

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.PL cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

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

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↗

arXiv2026

Noise-aware Verification and Synthesis of Quantum Programs

This work provides a comprehensive framework for noise-aware quantum program analysis, ranging from logical foundations to model checking and automated synthesis. While most research on quantum programming considers an idealized, noise-free semantics for quantum programs, we reason about quantum programs that are executed on real, noisy hardware. We use the error models published by quantum-hardware vendors to give a hardware-dependent semantics to quantum programs. We then present a noise-aware quantum Hoare logic with a relatively complete proof system. We finally use state-space exploration techniques for the hardware-aware verification and synthesis of loop-free quantum programs. In this way, we synthesize optimal, hardware-dependent solutions for parity bit-flip, GHZ state preparation, and other problems that commonly occur as subroutines in larger quantum algorithms. We evaluate our method on all 55 hardware specifications provided by the IBM Qiskit toolkit. Finally, we also show that classical probabilistic branching is needed for optimality in quantum programming.

cs.PL↗

arXiv2026

Record Types Everywhere

This paper introduces a novel calculus that models first-class environments and function application paradigms using standard record types. By proposing new extensions to general record types, we achieve a design that is remarkably simple and principled. We formalise this design in a core calculus and prove several desirable properties, including type soundness, normalization, and a simulation of the simply typed lambda calculus. Additionally, we extend the design with mutable references. The calculus, its semantics, along with the extension, and all stated properties are fully mechanized in the Lean 4 proof assistant, alongside an interpreter formally verified to be equivalent to the operational semantics.

cs.PL↗