Soundly Handling Linearity
Programming languages can statically ensure that certain resources are used exactly once through a linear type system based on Girard’s linear logic. Typical linear type systems track the number of times that variables are used under the assumption that continuations are always used linearly. Alas, this assumption is false in programming languages with powerful non-linear control flow features. For instance, in POSIX C the process duplication function `fork()` returns to its caller twice. More generally control operators such as Plotkin and Pretnar’s effect handlers, as in the web-programming language Links, enable the programmer to capture a continuation and then invoke it more than once or drop it altogether.
