meta
Compile-time programming — tokens, AST, reflection, quote, capability contexts.
proof
Proof-carrying code bundles and refinement reflection — every public type.
mathesis
∞-Topos of formal theories — Yoneda loading, Kan translation, descent coherence.