Quick links

Linear Logic, Heap-shape Patterns and Imperative Programming

Report ID:
June 2006
Download Formats:


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.

Follow us: Facebook Twitter Linkedin