Linear Logic, Heap-shape Patterns and Imperative Programming
|Authors:||Jia, Limin, Walker, David|
In this paper, we propose a new programming paradigm designed to simplify the process of safely creating, manipulating and disposing of complex mutable data structures. In our system, programmers construct data structures by specifying the shapes they want at a high level of abstraction, using linear logical formulas rather than low-level pointer operations. Likewise, programmers deconstruct data structures using a new form of pattern matching, where the patterns are again drawn from the syntax of linear logic. In order to ensure that algorithms for construction, inspection and deconstruction of heap values are well-defined and safe, we analyze the programmer's linear logical specifications using a mode analysis inspired by similar analysis used in logic programming languages. This mode analysis is incorporated into a broader type system that ensures the memory safety of the overall programming language.