A theory of substructural types and control

Jesse A. Tov*, Riccardo Pucella

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

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).

Original languageEnglish (US)
Title of host publicationOOPSLA'11 - Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications
Pages625-641
Number of pages17
DOIs
StatePublished - Nov 23 2011
Event2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA'11 - Portland, OR, United States
Duration: Oct 22 2011Oct 27 2011

Publication series

NameProceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA

Other

Other2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA'11
Country/TerritoryUnited States
CityPortland, OR
Period10/22/1110/27/11

Keywords

  • Languages

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'A theory of substructural types and control'. Together they form a unique fingerprint.

Cite this