LFCS Seminar: 4 May 2021 - Jonathan Brachthäuser, EPFL

Title: All About That Stack: A Unified Treatment of Regions and Control Effects

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 behaviour. 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 sub-regioning 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.

Joint work with Philipp Schuster and Klaus Ostermann