Erasure, dependent protocols, effects, specifications, and partiality

The paper calculus has one closed universe, ordinary dependent typing, a separate grade-vector usage judgment, strong and weak sums, naturals, empty elimination, the configurable predicates $\mathsf{Prodrec}$ and $\mathsf{Emptyrec}$, and the paper’s ${\mathsf{nr}}_{p,r}$ laws. Usage substitution is matrix multiplication, and theorem 101.6 proves usage preservation for the exact displayed reduction rules. The imported normalization and conversion result, theorem 101.7, uses tag jfp-submission-2026-04-30, commit 75c23df3b1421184cffe35ffd492bb9743dff240. That tag is a larger parameterized formalization. The chapter restricts its consequence to the paper sublanguage: empty definition context, literal level zero, no equality reflection, the displayed type-former restrictions, and no term containing an additional constructor. It imports no consequence for a program using identity, opacity, weak-unit, or first-class-level syntax.

Operational erasure soundness, theorem 101.11, requires the well-behaved-zero conditions, the printed weak-pair-match restriction, and consistency when grade-zero empty elimination is admitted. The common-numeral conclusion is distinct from the heap/stack theorem theorem 101.13, which belongs to the separate recursion calculus with greatest-lower-bound recursion grades. The Kappa corpus checks six finite extraction decisions; it proves none of these metatheorems.

The process calculus combines a total dependent functional language with intuitionistic linear sessions, persistent and disjoint linear channel contexts, term sessions $\mathrm{\$}\tau$, shared services $!A$ with Copy, and dependent $\mathrm{\forall }/\mathrm{\exists }$ protocol quantifiers. Functional substitution changes every index; channel substitution composes one provider and one client. A shared-service cut may answer a copy request while retaining its replicated provider, but no linear declaration is duplicated. Type preservation in theorem 102.8 is for the displayed synchronous cut reduction system. Closed global progress in theorem 102.9 additionally requires empty functional, persistent, and linear environments, offered type $1$, and liveness. It supplies no asynchronous, multiparty, ATS, or resource-bound theorem. The separate ATS card has static protocol sorts and an index-driven $\mathsf{repeat}$ protocol; it supplies no theorem to the process calculus. The Kappa corpus checks six finite traces, including real endpoint-generation consumption and a bounded repeat unfolding, only.

The Fire Triangle theorem assumes unrestricted substitution and dependent Boolean elimination. It also assumes an internal Boolean context with both printed judgmental observability equations. Removing any vertex changes the theorem. The selected dCBPV fragment separates value and computation types and adds Bind${}^{+}$ with a thunk-indexed classifier. Subject reduction in theorem 103.10 excludes printing, global state, and erratic choice, requires thunkability at every dependent bind, and requires linearity at every effect interchange. Its reader and exception clauses are the bounded source instances named in the proof. A global read is not thunkable: the exact source rule is one-sided inclusion rather than classifier equality, so uniqueness of typing is not recovered. The CPS and computational Sigma comparisons use different signatures and donate no theorem to this fragment. The Kappa corpus computes its classifier from a recursive value/computation syntax, preserves both endpoints of the thunked read, checks inclusion separately from transition equality, and exercises eight finite cases. It does not prove that a sensitive classifier is preserved across global state.

Predicate transformers are the displayed pure, exception, state, and state-with-exception types with monotonicity and conjunctivity. The selective CPS theorem theorem 104.4 imports typing, monotonicity, conjunctivity, and equation preservation only for the exact $\mathsf{DM}$ grammar. Dijkstra computation typing generates verification conditions through WP-Sub. Total-correctness theorem theorem 104.7 requires a source-well-formed ${\mathrm{EMF}}^{\star }$ signature and normalization of its CIC target; it does not cover divergence, primitive concurrency, arbitrary handlers, an unverified action, or solver soundness. The Kappa corpus decides six finite state/exception postcondition cases.

The carrier $A^{\nu }$ has return and guarded step. Convergence is inductive, and weak equality records equality of convergence behavior. Theorem 105.8 is a monad theorem in setoids, not a raw constructor-equality theorem. Search adequacy in theorem 105.9 is an exact convergence criterion and does not decide convergence. The least-fixed-point result theorem 105.12 requires the printed finite-support property; its maximum-approximant argument fails without finitarity. The general-recursive language comparison is a separate calculus. The Kappa observer checks seven finite fuel observations and never interprets later as divergence.