Split Decisions: Explicit Contexts for Substructural Languages

Watch this 28-minute conference talk from CPP 2025 exploring "Contexts as Resource Vectors" (CARVe), a general syntactic infrastructure for managing substructural contexts in programming languages. Learn how researchers from McGill University and University of Milan address the central challenge of modeling contexts in substructural languages by using a system where elements are annotated with tags from a resource algebra denoting their availability. Discover how this approach allows for defining relations between substructural contexts via simultaneous substitutions without splitting them, and how it establishes algebraic properties about context operations needed for practical proofs. The presentation demonstrates CARVe's application through detailed reformulations of linear sequent calculus and bidirectional linear λ-calculus, proving their equivalence, and extends to diverse systems including affine λ-calculus and session-typed process calculus CP. Implemented in the proof assistant Beluga, this work offers valuable best practices for mechanizing a wide range of substructural systems.