Adoption and focus: practical linear types for imperative programming Export

@inproceedings{citeulike:70952, abstract = {A type system with linearity is useful for checking software protocols andresource management at compile time. Linearity provides powerful reasoning about state changes, but at the price of restrictions on aliasing. The hard division between linear and nonlinear types forces the programmer to make a trade-off between checking a protocol on an object and aliasing the object. Most onerous is the restriction that any type with a linear component must itself be linear. Because of this, checking a protocol on an object imposes aliasing restrictions on any data structure that directly or indirectly points to the object. We propose a new type system that reduces these restrictions with the adoption and focus constructs. Adoption safely allows a programmer to alias objects on which she is checking protocols, and focus allows the reverse. A programmer can alias data structures that point to linear objects and use focus for safe access to those objects. We discuss how we implemented these ideas in the Vault programming language.}, address = {New York, NY, USA}, author = {Fahndrich, Manuel and Deline, Robert}, booktitle = {PLDI '02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation}, citeulike-article-id = {70952}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=512529.512532}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/512529.512532}, doi = {10.1145/512529.512532}, isbn = {1-58113-463-0}, issn = {0362-1340}, keywords = {imperative-programming, linear-logic, types}, location = {Berlin, Germany}, month = {May}, number = {5}, pages = {13--24}, posted-at = {2006-10-06 12:05:32}, priority = {2}, publisher = {ACM}, title = {Adoption and focus: practical linear types for imperative programming}, url = {http://dx.doi.org/10.1145/512529.512532}, volume = {37}, year = {2002} }

TY - CONF ID - citeulike:70952 L3 - citeulike-article-id:70952 N2 - A type system with linearity is useful for checking software protocols andresource management at compile time. Linearity provides powerful reasoning about state changes, but at the price of restrictions on aliasing. The hard division between linear and nonlinear types forces the programmer to make a trade-off between checking a protocol on an object and aliasing the object. Most onerous is the restriction that any type with a linear component must itself be linear. Because of this, checking a protocol on an object imposes aliasing restrictions on any data structure that directly or indirectly points to the object. We propose a new type system that reduces these restrictions with the adoption and focus constructs. Adoption safely allows a programmer to alias objects on which she is checking protocols, and focus allows the reverse. A programmer can alias data structures that point to linear objects and use focus for safe access to those objects. We discuss how we implemented these ideas in the Vault programming language. CY - Berlin, Germany IS - 5 SN - 1-58113-463-0 AD - New York, NY, USA EP - 24 TI - Adoption and focus: practical linear types for imperative programming PB - ACM VL - 37 T2 - PLDI '02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation SP - 13 KW - imperative-programming KW - linear-logic KW - types AU - Fahndrich, Manuel AU - Deline, Robert PY - 2002/05// UR - http://dx.doi.org/10.1145/512529.512532 ER -