Cross-reference glossary for README.adoc, EXPLAINME.adoc, and the ideas-to-alphas wiki.
- Incubator (idea → alpha)
-
The middle stage of the type theory pipeline: artefacts from Kategoria (lab) are matured from speculative idea to tested alpha before earning promotion to Typell (production kernel). Classification: project-specific (governance pattern).
- Graduation
-
The promotion of an artefact from the incubator to a production repository. A human decision based on proof stability, downstream readiness, and review. Not automated. Classification: project-specific (governance pattern).
- Port-and-reprove
-
The pattern where downstream repositories re-prove results in-site rather than importing from the incubator. Ensures production code does not depend on unstable research artefacts. Classification: project-specific (estate pattern). Precedent:
typed-wasm/…/Tropical.idr.
- Type theory pipeline
-
The end-to-end flow: Kategoria (lab) → ideas-to-alphas (incubator) → Typell (kernel) → typed-wasm (target) → PanLL (environment). Each stage has increasing stability guarantees. Classification: project-specific (organisational architecture).
- Proof-of-concept
-
A formalisation that compiles and type-checks but may not cover all obligations, may use simplifying assumptions, and carries no stability guarantee. The standard artefact of the incubator. Classification: standard (methodology).
- Experimental type-safety level
-
A candidate for a type-safety level beyond L10 (e.g., graded types, effect types, modal types). Defined speculatively here; may be retracted, merged, or promoted. Classification: project-specific (speculative).
- Research note
-
Annotated reading notes on papers being formalised. Not publications; working documents for the incubator’s own use. Classification: standard (practice).
- a-sounder-constitution
-
An Idris 2 formalisation of soundness constraints for the type theory pipeline. A constitutional scaffold: a statement of what the pipeline intends to prove, with initial proof structure. Classification: project-specific (proof-of-concept).
- silo (secret-silo)
-
An incubated design for ALARP (as low as reasonably practicable) handle/vault secret management. Not yet promoted. Classification: project-specific (incubated design).