TY - GEN
T1 - A theory of substructural types and control
AU - Tov, Jesse A.
AU - Pucella, Riccardo
PY - 2011
Y1 - 2011
N2 - Exceptions are invaluable for structured error handling in high-level languages, but they are at odds with linear types. More generally, control effects may delete or duplicate portions of the stack, which, if we are not careful, can invalidate all substructural usage guarantees for values on the stack. We have developed a type-and-effect system that tracks control effects and ensures that values on the stack are never wrongly duplicated or dropped. We present the system first with abstract control effects and prove its soundness. We then give examples of three instantiations with particular control effects, including exceptions and delimited continuations, and show that they meet the soundness criteria for specific control effects. Copyright is held by the author / owner(s).
AB - Exceptions are invaluable for structured error handling in high-level languages, but they are at odds with linear types. More generally, control effects may delete or duplicate portions of the stack, which, if we are not careful, can invalidate all substructural usage guarantees for values on the stack. We have developed a type-and-effect system that tracks control effects and ensures that values on the stack are never wrongly duplicated or dropped. We present the system first with abstract control effects and prove its soundness. We then give examples of three instantiations with particular control effects, including exceptions and delimited continuations, and show that they meet the soundness criteria for specific control effects. Copyright is held by the author / owner(s).
KW - Languages
UR - http://www.scopus.com/inward/record.url?scp=81455159343&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=81455159343&partnerID=8YFLogxK
U2 - 10.1145/2048066.2048115
DO - 10.1145/2048066.2048115
M3 - Conference contribution
AN - SCOPUS:81455159343
SN - 9781450309400
T3 - Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA
SP - 625
EP - 641
BT - OOPSLA'11 - Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications
T2 - 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA'11
Y2 - 22 October 2011 through 27 October 2011
ER -