Reasoning about Mutability in Graded Modal Type Theory

Abstract

Pure functional programming enables easier maintainability, parallelism, and reasoning about programs. However, mutable state has historically been at odds with the functional paradigm. Linear types provide a way to safely integrate mutable state into functional programming languages. This thesis explores the intersection of functional programming and mutable state, focusing on the challenges and innovations surrounding mutable arrays in languages with linear or uniqueness types. We present a partial formalization of a graded lambda calculus with array primitives. Graded modal types are used in an attempt to show that efficient mutable operations are safe. We tried to prove bisimilarity between copying and mutable operational semantics, but the proof is not complete.