In Proc. 26th ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’11), Oct. 2011.
- Slides from
OOPSLA talk (PDF, 6.4 MiB)
- LaTeX source (tar.gz, 4.6 MiB)
- Shorter version (as in OOPSLA’11):
- color (PDF, 432 KiB)
- black and white (PDF, 430 KiB)
- Extended version (full proofs):
- color (PDF, 863 KiB)
- black and white (PDF, 856 KiB)
- DOI: 10.1145/2076021.2048115 (ACM paywall)
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 © 2011 ACM. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior specific permission and/or a fee.