Dependent subtyping, object paths, and classical control

The $\lambda P_{\le }$ import uses the Church-style calculus of Compagnoni and Aspinall. It has dependent kinds and products and bounded type variables. It also has type abstraction, type application, two beta relations, and well-kinded inputs. Its imported boundary is narrowing, substitution, reduction closure, sound and complete algorithmic subtyping, and decidability of the printed formation, kind, minimal type inference, and subtyping judgments. $\mathsf{DRef}$ is instead the locally proved, fully annotated difference constraint calculus; decidability assumes well-scoped finite graphs and replayed path certificates. The Fire Triangle assumes an STLC fragment, a universal unknown, CIC conservativity, and gradual embedding and projection behavior. The GCIC import is specifically CastCIC${}_G$: it supplies elaboration, type safety with error outcomes, CIC conservativity, observational graduality, and embedding and projection laws, but no normalization theorem. The list/vector partial connection is a separate representation boundary. The Kappa corpus checks eleven finite, tagged ledger outcomes and proves none of these metatheorems.

The selected DOT system has A-normal syntax and variable paths. It is the calculus of Rapoport, Kabir, He, and Lhoták, with recursive self, intersections, tight type members, dependent functions, and no recursive-type subtyping rule. The imported lemmas are selection replacement, general-to-tight and tight-to-invertible conversion, canonical forms, replacement narrowing, variable substitution, progress, and preservation at that exact syntax and reduction. The cited Coq tree mechanizes the named structural components but does not replay termination of the paper’s greedy longest-evaluation-context construction. Hu–Lhoták’s algorithmic boundary says full subtyping and term typing are undecidable, while the named kernel and strong-kernel fragments are decidable; it does not make full DOT algorithmic. The Kappa corpus decides finite inertness and equal-bound selection only.

pDOT extends the preceding inert/tight staging with stable immutable field paths, singleton path types, one-occurrence path replacement, precise path-indexed initialization, and store-indexed path lookup. The chapter’s formation-indexed $\mathrm{RPath}$ and $\mathrm{Replace}$ relations check every changed target prefix and the complete changed selected type; proposition 108.4 proves this local strengthening admissible in the source’s raw replacement system. The exact Def-New rule has only its intrinsically well-formed body and tight-record premises. The function-path lookup lemma and the imported safety theorem are exactly those of Rapoport and Lhoták: ordinary progress may stop at a typed path, extended reduction continues lookup to a value, and one-step term reduction preserves typing while extending a matching inert, well-formed runtime context. The import does not state decidability, cover mutable paths or full Scala, or prove termination of arbitrary well-typed path lookup. The cited 23-file Coq artifact proves the source’s safety and extended_safety results at its historical toolchain. The Kappa corpus is a bounded finite lookup and prefix-formation checker only.

The source is Miquey’s $d{L}_{\widehat{\mathsf{tp}}}$. Regular proofs, contexts, and commands carry no dependency list. Only dependent contexts and commands involving $\widehat{\mathsf{tp}}$ carry the list $\sigma$, whose compatibility classes reconcile the two formulas of a dependent cut. The proof premise of that cut remains regular. The exact signature also includes the mutually inductive NEF grammar $p_N,c_N,e_N$, and the distinguished dependent continuation. In the NEF grammar, $\mu \star .c_N$ is distinct from an ordinary $\mu \alpha .c$, and $e_N$ is generated only by $\star$ and $\tilde{\mu }a.c_N$. Subject reduction is imported from Theorem 3.2. The dependent NEF translation is the proof component of Lemma 4.9, and simultaneous CPS type preservation is Proposition 4.10 at the source’s exact intuitionistic target signature. Strong normalization uses the administrative simulation and termination measure of Propositions 4.2, 4.5–4.7 and Theorem 4.8; consistency additionally uses Proposition 4.10 and Theorem 4.11. The results admit classical control in programs but do not admit $\mu$-proofs or application spines inside formula dependencies. They assert neither equality reflection nor unrestricted classical witness extraction. The Kappa corpus checks twelve finite grammar and type-skeleton observations, not the calculus or its CPS metatheory.