Is there a use for linear logic?

Abstract

Past attempts to apply Girard's linear logic have either had a clear relation to the theory (Lafont, Holmstr6m, Abramsky) or a clear practical value (Guzmiin 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. © 1991, ACM. All rights reserved.