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.