Linear types, protocols, and processes in classical F°

Session types and typestate both promise a type system that can reason about protocol adherence. The complexity budgets of most programming languages, however, do not allow for new forms of types aimed at specific problem domains—even domains as broad as these. Classical F°—read F-pop —is a typed λ-calculus based on classical (i.e., full) linear logic, wherein session types arise naturally from the interaction between the usual sums, products, and implications of linear logic and a simple process model, with the dualizing negation of classical logic naturally accounting for how a protocol is seen by each of a channel\u27s endpoints. Classical F° expressions evaluate to processes, reminiscent of those in the π-calculus, that communicate over channels, but source expressions, rather than including processes and channels, employ only two novel control operators that account for process creation and communication. F° is introduced by way of its intuitionistic fragment, which even on its own can account for typestate: the combination of linearity and polymorphism leads to natural encodings of many programmer-specified protocols. In fact, any protocol expressible as a regular language can be encoded in an intuitionistic F° type. F° distinguishes between linear and unrestricted types by using kinds together with a notion of subkinding, avoiding the pitfalls of approaches based on type qualifiers or modalities; kinds are related by a subkinding order that allows unrestricted types to be treated as though they were linear. Soundness for intuitionistic and classical F° is proved both in the standard operational sense of preservation and progress and for an augmented semantics that shows more directly that the expected properties of linearity are preserved. This establishes the absence of deadlocks in closed, well-typed F° programs; it also guarantees that such programs will not leak processes as long as their result types are unrestricted