Is There a Use for Linear Logic

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 (Guzman and Hudak, Wadler), but not both. This paper denes a sequence of languages based on lin-ear logic that span the gap between theory and practice. Type reconstruction in a linear type sys-tem can derive information about sharing. An ap-proach to linear type reconstruction based on use types is presented. Applications to the array up-date problem are considered.