nextgen-typing is the coordination monorepo for the hyperpolymath type
theory pipeline. It does not contain compiler or application code; it
documents and coordinates the pipeline, and hosts the cross-project
formal-verification proofs in verification/proofs/. It documents, connects,
and tracks the pipeline:
katagoria → typell → typed-wasm → PanLL (research) (kernel) (target) (eNSAID env)
The type theory work spans multiple repos: * typell — the verification kernel (Rust, ~14 crates) * typed-wasm — WasmGC type safety + aggregate library (Idris2, Zig) * tropical-resource-typing — foundational tropical type theory (Isabelle, Lean 4) * protocol-squisher — transport semilattice (tropical connection) * katagoria — research origination space (created 2026-04-11, active)
These repos are logically one pipeline. Without a coordination layer, AI
agents and developers working in any single repo lack context for the others.
nextgen-typing is that context: one place to read the full architecture.
This repo makes no claims about compiler correctness, proof soundness, or benchmark results. Those claims are made and verified in the constituent repos. Here we only document:
-
The pipeline structure and how repos relate
-
Architectural decisions that span repos (e.g. "TypeLL is open-ended")
-
Research artefacts that don’t belong in a single repo
| File | What’s There |
|---|---|
|
Pipeline overview: the main chain, co-products, key architectural decisions |
|
What’s done and what needs doing: katagoria (created), constituent repo updates, research work |
|
Full pipeline architecture doc (also served as the creation briefing) |
|
Current state: milestones, blockers, next actions |
|
ADRs: open-ended TypeLL, dual-role typed-wasm, katagoria upstream |
|
All related projects and their relationship types |