Spegion: Implicit and Non-Lexical Regions with Sized Allocations
Jack Hughes, Michael Vollmer, Mark Batty

TL;DR
Spegion introduces an implicit, effect-based region management system with sized allocations, enabling safe, fine-grained memory control without explicit annotations or substructural types.
Contribution
It presents Spegion, a novel language that achieves safe, non-lexical region management with a concise syntax and effect system, avoiding complex type systems.
Findings
Type safety is proven for Spegion's system.
Supports fine-grained, sized region allocations.
Enables implicit, non-lexical memory management.
Abstract
Region based memory management is a powerful tool designed with the goal of ensuring memory safety statically. The region calculus of Tofte and Talpin is a well known example of a region based system, which uses regions to manage memory in a stack-like fashion. However, the region calculus is lexically scoped and requires explicit annotation of memory regions, which can be cumbersome for the programmer. Other systems have addressed non-lexical regions, but these approaches typically require the use of a substructural type system to track the lifetimes of regions. We present Spegion, a language with implicit non-lexical regions, which provides these same memory safety guarantees for programs that go beyond using memory allocation in a stack-like manner. We are able to achieve this with a concise syntax, and without the use of substructural types, relying instead on an effect system to…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
