AARA and protocol theorem boundaries

Polynomial AARA

Signature.

First-order call-by-value RAML in let-normal form, affine contexts, terminating stack/heap big-step evaluation, nonnegative rational degree-bounded annotations, and the fixed allocation metric $K^{\mathsf{pair}}=K^{\mathsf{cons}}=1$ with every other cost zero.

Theorem.

Given a well-formed stack/heap, an existing terminating evaluation, a typing derivation, and slack $r\ge 0$, every counter $q\ge {\mathrm{\Phi }}_{V,H}(\mathrm{\Gamma })+p+r$ yields the same result with a residual counter at least ${\mathrm{\Phi }}_{H^{\prime }}(v:A)+p^{\prime }+r$.

Not claimed.

Termination, inference completeness, tightness, a theorem about RAML 1.5, or transfer from evaluation-step polynomials to heap cells.

Binary logical sessions and graded non-linearity

Logical signature.

The finite intuitionistic linear process calculus with one offered channel, linear and unrestricted contexts, synchronous cut reduction, and the displayed connectives. Preservation retains the same judgment. Global progress requires the exact closed $\cdot ;\cdot ⊢P::x:\mathbf{1}$ and liveness hypotheses.

Recursive extension.

The linear fragment has contractive, tail-recursive equi-recursive types and coinductive equality; the auxiliary endpoint dual is not defined on unrestricted $!A$. Every transmitted type is closed with respect to surrounding recursion variables, so naive syntactic duality commutes with unfolding. The chapter does not extend that operation to arbitrary contractive types.

Graded journal signature.

A distinct calculus of typed terms, processes, channel configurations, runtime contexts, and resource allocation. Its progress theorems require the buffered invariant; its preservation theorem yields a post-context. Promotion primitives retain their exact SingleAction, ExactSemiring, ReceivePrefix, and Sends premises. $\mathsf{Graded}nP$ is a type function in the multicast signature, not a premise.

Not claimed.

General binary deadlock freedom, dependent protocols, the journal paper’s conjectural deadlock result, or equivalence with the earlier Granule implementation.

Repaired MPST and Pirouette

MPST signature.

The ECOOP 2025 process calculus has located sessions, explicit FIFO addresses, sender-tagged values/endpoints/labels, closed contractive global and local types, partial plain projection, asynchronous global/local semantics, and typed concrete queues.

MPST theorem.

A global type is unstuck when every relaxed barb has a true labelled transition to another unstuck type; coherence adds projectability and linearity and is lifted through projection and path decomposition. Under that exact coherence, one process step preserves typing with existential post-environments and either leaves the coherent global state fixed or advances it by one label. Communication safety is the only behavioral corollary imported here.

Pirouette.

Its signature has synchronous higher-order choreographies with location-indexed local expressions, selection, communication, procedures, block sets, out-of-order steps, control programs, merge, and endpoint projection, parameterized by the fully stated local-language interface.

Theorems.

Local preservation yields relative preservation; Boolean inversion and local progress yield relative progress. Global projection soundness additionally assumes $\mathrm{LN}(C)\subseteq L\ne \varnothing$. Deadlock freedom applies only to systems reached from a choreography satisfying the source predicate $\mathsf{PirExprClosed}(C)$ and the displayed typing judgment, under a choreography type system with progress and preservation. The mechanized theorem and the chapter statement retain its three load-bearing boundary hypotheses: the projection location list is nonempty, it covers every location in the choreography, and the choreography is closed.

Mechanization pins.

The MPST Coq identifiers were checked at commit 6d5362df12b049b79b3a28b4519c28f7d0ee4831; Pirouette at 16090ca5a03d8d28604274b4c8146651f0185f2c; and the Granule version map at e4aba0d6c1d6d1c0bda10a81f6ae1365f2ad62f5.

Not claimed.

The historical HYC proof does not own subject reduction. Pirouette does not establish asynchronous queue liveness, arbitrary endpoint equivalence, failure recovery, or network-runtime correctness.