Past attempts to apply Girard’s linear logic have either had a clear relation to the theory (Lafont, Holmström, Abramsky) or a clear practical value (Guzmán 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.
|Title of host publication||Proceedings of the 1991 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation|
|Number of pages||19|
|Publication status||Published - 1 May 1991|