nextgen-typing Roadmap

Table of Contents

Near-Term (This Sprint)

✓ Create katagoria repo from rsr-template-repo
✓ Fix TypeLL docs: remove "10 levels" framing → "open-ended progressive" (typell/ROADMAP.adoc)
✓ Add typed-wasm reference to nextgen-languages/ monorepo
✓ Write/clean up docs/ARCHITECTURE.adoc (pure architecture doc, no briefing framing)
✓ Add docs/PIPELINE.adoc (machine-readable A2ML pipeline spec)
✓ Populate .machine_readable/6a2/ files with real project state (STATE, META, ECOSYSTEM)
✓ Add nextgen-typing + katagoria ecosystem references to typell and typed-wasm ECOSYSTEM.a2ml
✓ Add ecosystem references to all constituent repos (affinescript, ephapax, tropical-resource-typing, protocol-squisher)
✓ katagoria: first research artefact structure (research/level-candidates/)
✓ protocol-squisher ECOSYSTEM.a2ml migrated from SCM format to A2ML
✓ typed-wasm ABI conventions implementation (layout proofs in src/abi/layout/ — DecEq, nullability, distinctness, passConvention + proofs, Stdlib)

✓ Formalise Protocol Squisher tropical connection (protocol-squisher/proofs/tropical/)
✓ katagoria: first research artefact — L11-modal-box (Idris2 sketch, MOTIVATION.adoc)
✓ katagoria L11-modal-box: comonad laws proved (Refl after case split — believe_me-free)
✓ typed-wasm DecEq: DecEq (a, b) instance added — WHT_Struct resolution chain complete
✓ protocol-squisher tropical: foldl-min optimality proved (foldl_tcAdd_le_init/mem + minimax_path_optimal)
✓ typed-wasm layout: WasmGC recursive types — WHT_Var/WHT_Rec added; List self-reference correct
❏ Extend Tropical.thy: linorder instance, tropical matrices, Kleene algebra
❏ Write arXiv paper on speculative tropical session types
❏ typed-wasm ABI conventions for AffineScript + Ephapax cross-language calls (pending recursive types)