Is there a use for linear logic?
Philip L. Wadler · 1991
Past attempts to apply Girard's linear logic have either had a clear relation to the theory (Lafont, Holmstrom, Abramsky) or a clear practical value (Guzm'an and Hudak, Wadler), but not both. This paper defines a sequence of languages based on linear logic that span the gap between theory and practice. Type reconstruction in a linear type system can derive information about sharing. An approach to linear type reconstruction based on use types is presented. Applications to the array update problem are considered. 1 Introduction Storage reuse; single threading; in-place update; sharing analysis; linearity: any problem with so many names must be important. Girard's linear logic has intrigued computer scientists with its promise to focus new light on this old subject. (It also hints at enlightenment with regard to parallelism, but that's a topic for other papers.) Attempts to apply linear logic fall into two camps, the theoreticians and the practitioners. On the theoretical side sit Lafo...