Date of Award
Doctor of Philosophy
Tian Zhao, Christine Cheng, Chris Hruska, Hong Yu
Aliasing, Fractional Permissions, Linear Type, Mechanized Proof, Mutable State, Type System
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.
Sun, Chao, "A Conservative Type System Based on Fractional Permissions" (2016). Theses and Dissertations. 1210.