\emph{Context.} Behavioural type systems such as session types, typestate, and mailbox types allow a developer to specify and check behavioural properties within their application code, giving programs that are correct-by-construction. Session types in particular allow a developer that communication in their code follows pre-defined protocols.

\emph{Inquiry.} Implementing session types in functional languages requires some form of resource control, most commonly achieved through the use of linear typing. However, linear type systems as specified declaratively \emph{cannot be implemented algorithmically}. Even when using techniques such as leftover typing, implementing other substructural modes (e.g., affine and relevant) requires ad-hoc changes to typing rules.

\emph{Approach.} We investigate \emph{co-contextual type systems} as a general framework for implementing substructural type systems. Whereas standard type systems require a type environment as an \emph{input} to a typechecking algorithm, \emph{co-contextual} type systems—a class of type system originally introduced for efficient incremental typechecking—produce a type environment and as an \emph{output} of the typechecking judgement.

\emph{Knowledge.} We show how to generalise co-contextual type systems to support algorithmic implementations of substructural typing: simple changes to typechecker parameters allow us to instantiate our typechecker to check unrestricted, linear, affine, and relevant $\lambda$-calculi. Building on this approach, we present a second language with an extended constraint system that can support mixed-linearity typing, and we use this to implement an algorithmic type system for the GV session-typed functional language.

\emph{Grounding.} We prove four instantiations of our algorithm sound and complete with respect to declarative unrestricted, linear, affine, and relevant $\lambda$-calculi. We prove our our co-contextual session typing algorithm sound and complete with respect to a declarative presentation of GV. Finally, we implement our typechecking algorithm in OCaml and demonstrate it on a series of case study applications.

\emph{Importance.} This work shows the versatility of co-contextual typing as a framework for supporting algorithmic implementations of substructural type systems, in addition to its originally-presented benefits (e.g., support for incremental and parallel typechecking). Our work further lays the groundwork for implementing programming languages with more sophisticated type combination operations that are out-of-reach of current approaches.