TL;DR
This paper characterizes global variables by unifying abstraction with region abstraction in a region-based language, connecting imperative operations with memory safety through linear protection.
Contribution
It demonstrates that the concept of global variables in a language called global can be derived from the region language by unifying abstraction and region abstraction.
Findings
Global variables are characterized via unification of abstraction and region abstraction.
Memory safety is achieved through linear protection in the global language.
The global language concept arises from the region language framework.
Abstract
We obtain a characterization of global variables by unifying abstraction with region abstraction in a region-based language. More precisely, in a previous work a language called global was presented, whose virtue is to provide a conceptually clear way of introducing imperative operations in a functional language. Memory safety is provided by the concept of linear protection, which connects the global system to a linear one. In this paper we show that the concept of global variable provided by the global language arises from the Tofte and Talping's region language through the unification of abstraction and region abstraction.
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.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Distributed systems and fault tolerance