A Conservative Type System Based on Fractional Permissions

Abstract

The system of fractional permissions is a useful tool for giving semantics to various annotations for uniqueness, data groups, method effect, nullness, etc. However, due to its complexity, the current implementation for fractional permissions has various performance issues, and is not suitable for real world applications. This thesis presents a conservative type system on top of the existing fractional permission type system. The system is designed with high-level types, and is more restrictive. The benefit is that it can run much faster. With this system, we propose a multi-tiered approach for type checking: the conservative type system is first applied, and only those that it cannot handle will then be processed by the more powerful fractional permission system. A crucial property about a type system is its soundness. In this thesis we also present a mechanized proof, written in Twelf, for the conservative type system. A mechanized proof is checked by computer, and offers much more confidence about its correctness. Moreover, we proved the soundness property with a novel approach: instead of defining the semantics of the language and proving progress and preservation directly, we delegate it to the soundness proof of the fractional permission system. The novel technical features in this thesis include: 1) a multi-tiered approach for type checking and a conservative type system build on top of fractional permissions; 2) a mechanized proof for the type system, and 3) a novel way of proving soundness property for a type system.