Computational meanings and untrusted Timpl front ends

Frozen Nuprl-style card and the quotient extension

Signature.

The principal card is the lazy untyped computation and PER closure frozen in convention 91.1: integers, dependent functions and pairs, equality, set types, and its displayed universe hierarchy. It is not an intrinsic Timpl signature. The source snapshot commit is $$\mathtt{\text{cfb69727c6af64c9bb15}}\mathtt{\text{7e89fded5e4a791d45f5}}.$$ The pinned default artifact build assumes FunctionalChoice_on in the metatheory.

Equality and universes.

Each closed type assigns a PER; open judgments quantify over pairs of equal substitutions. Equal types assign the same member relation. Universe stratification is exactly the Allen/Nuprl PER construction of definition 91.7, equation 91.6; it does not import the judgmental Russell-universe rules of $T_0$. Univalence and computed univalence are not in the signature.

Tfam/Trec/Tco.

Not in the printed signature. Derived naturals are the nonnegative-integer set, not an inductive family. The displayed successor is an ordinary lazy program. No coinductive rule is present.

Imported from the pinned artifact.

In per/sequents.v, the exact theorem is $$\mathtt{\text{sequent\_true\_eq\_VR}}.$$ It equates the artifact’s two global sequent meanings; theorem 91.23 records that import and its intermediate formulations.

Proved locally.

PER closure is theorem 91.8, and closure/member computation stability is theorem 91.12. The fixed-level local list meaning agrees with the local two-substitution judgment by proposition 91.25. No theorem identifies the global artifact relation with one ${\mathcal{C}}_i$. The dependent-function, dependent-pair, equality, and set rules are derived in theorem 91.26, theorem 91.27. Derived-natural typehood, canonicity, the two successor specifications, and computational consistency are lemma 91.17, theorem 91.18, theorem 91.30, theorem 91.31, theorem 91.32.

Normalization and decidability.

Not claimed. Lazy evaluation is a partial relation and the card includes divergent programs. The finite Kappa companion is implemented only and decides only its named closed fragment.

Separate extension.

Quotient data, its PER/well-definedness theorem, and its displayed rules are proved locally in theorem 91.38, proposition 91.39. Those rules use the explicit extension ${\mathcal{C}}_i^{\mathsf{q}}$ and its superscripted judgments, while every relation program $E(a,b)$ is typed and tested for inhabitance in the old ${\mathcal{C}}_i$ system. That extension repeats the nonuniverse base generators over extended premises, so dependent formers may range over quotient types. It retains the old universes unchanged and uses fresh ${\mathcal{U}}_i^{\mathsf{q}}$ tags for the expanded hierarchy. Theorem 91.38 proves PER assignment, type symmetry, transitivity, unique valuation, computational stability, and the exact one-way embedding for this extension. Lemma 91.37 is the level-coherence step for inherited versus freshly generated quotient triples. The extension is not in the pinned artifact’s close relation and no mechanized quotient soundness claim is transferred.

Timpl elaboration

Signature and delta.

$T_{\mathsf{elab}}$ is an untrusted surface layer over the Timpl kernel. It adds explicit/implicit syntax, contextual term metavariables, level metavariables, typed object constraints, strict level equalities, and formation lower bounds. It adds no kernel former, conversion rule, recursion rule, or equality principle.

Universe and equality assumptions.

Levels are zero/successor/maximum expressions. Their canonical atom normal form and exact equality decision are definition 112.9, lemma 112.10; their stratified solver is definition 112.12. Object constraints use Timpl judgmental equality. Total normalization, inversion, and conversion for the exact Timpl signature are an explicit interface hypothesis of convention 112.1; they are discharged for that exact signature by theorem 111.76, theorem 111.81, corollary 111.82, including demand D4. The elaboration chapter invokes those named operations through the interface and does not re-prove them.

Proved locally.

Constraint generation preserves typing by lemma 112.8, theorem 112.26. Direct contextual-pattern simplification terminates, immediately orients and substitutes every strict level equality it emits, and returns a genuinely typed most general object substitution, by theorem 112.24. The bound phase then decides the accumulated formation residue and returns the pointwise least bound assignment by theorem 112.13; least levels are not ordered by object instantiation. Candidate object assignments whose typing itself awaits such a residual bound are outside the direct fragment. Elaboration soundness is corollary 112.29; certificate completion and independent rechecking are definition 112.27, lemma 112.28. Completeness is only the policy-aligned theorem theorem 112.32. The direct solver’s three outcomes are success, unsatisfiable, and outside the direct fragment; the last is not a negative certificate.

Status boundary.

General higher-order unification, dynamic postponement, coercions, overloading, recursive clauses, and full-Timpl unconditional total elaboration are open or not in the signature as stated in section 112.8. The optional polymorphic-recursion derivation and source-firewalled UniCoq comparison import no theorem into Timpl; in particular, the latter includes overloading and guarded fixpoints and has no claimed correctness proof. Its archived source is pinned at tag v1.6-9.1, commit 450d91a5a2a32a9a 953efd703418e7ab b5675f1e. In a fresh copy, Rocq 9.1.1 with OCaml 5.4.1 successfully ran

rocq makefile -f _CoqProject -o Makefile.audit
make -f Makefile.audit -j2

and produced the plugin, its theory, and all eight listed test objects, including executable runs of primitive.v and bug_41.v. This is source-specific behavior evidence, not a proof of the paper’s correctness conjecture. The Kappa companion is implemented only and checks the six named finite cases.

Timpl-clauses

Signature and delta.

Timpl-clauses is the ordered, first-order source layer of definition 121.1. It adds variables, constructor patterns, inaccessible terms, absurd patterns, leftmost splitting, and direct-child structural calls. Its target is a typed case tree translated to existing Timpl eliminators. It adds no kernel conversion, identity, universe, recursion, or coinduction rule.

Equality and family assumptions.

Index refinement uses the restricted homogeneous unifier and no-K case-tree interface inherited from definition 78.9. Generated judgmental equations are exactly reachable leaf equations; overlapping later rows receive only their residual equations. Identity remains intensional and univalence is not in the signature.

Proved locally.

Compiler termination, relative to termination of every scheduled restricted-unifier call and its weak-head computations, is lemma 121.13; specialization and target typing are lemma 121.14, theorem 121.17. Coverage and its qualified symbolic failure witnesses are theorem 121.19. Exact equation generation and closed-data source/target simulation are proposition 121.21, theorem 121.23. The simulation distinguishes static or erased closed normal forms from relevant runtime values. It uses the chapter’s explicit left-to-right runtime contexts, including the source-only frame that evaluates the next relevant argument of a declared call. The target has the beta, projection, Boolean, natural-number, identity, and vector root computations; the source alone adds least-matching-row contraction. Its proof first establishes one-step simulation after the administrative beta contractions introduced by replacing the declared head with its compiled target, then inducts on the length of the finite source reduction.

Status boundary.

Normalization, canonicity, consistency, conversion, and erasure are inherited only when their separate Timpl theorems apply; this chapter proves none upward. Agda and Equations are comparison artifacts, not theorem sources. The Kappa companion is implemented only for the five named finite declarations.