by Philipp Schuster, Jonathan Immanuel Brachthäuser, and Klaus Ostermann

Technical report. University of Tübingen, Germany, 2021.

This publication is related to the Effects research project.

Abstract

Ever since the inception of Algol have programming language researchers sought good abstractions to inspect and manipulate stacks while maintaining basic invariants of program behavior. These abstractions range from procedure calls and block structure to region-based resource management and control effects. While all these abstractions are useful and well-designed individually, their combination and interaction is an open issue. We present a conceptual framework with a novel form of stack abstraction, in which stacks are decomposed into regions, moves between stacks are expressed as control effects, and relationships between regions are represented with subregioning evidence. We demonstrate and prove that these abstractions are powerful enough to express and combine region-based resource management and control effect while guaranteeing region and effect safety invariants. We also discuss an implementation by means of a compilation to System F and validate its utility by means of several standard examples.