eval
Call-by-push-value term algebra — foundations for effects and evaluation strategies.
control
Delimited continuations — shift / reset term algebra.
concurrency
π-calculus processes and session types — formal concurrency foundations.
logic
Modal logic (Kripke) and linear logic — the metatheory behind session types, capabilities, and affine modifiers.
core.types — advanced type-system primitives
Polymorphic kinds, quantitative type theory (QTT), and two-level type theory (2LTT) — the research-grade vocabulary on which the verification layer and higher-kinded libraries build.
core.action — DC-side Diakrisis enactments
The Dependency-Centric half of the AC/OC duality. Articulations, enactments, ε-primitives, monads, ludics, and the gauge canonicalisation.