Date of Award

May 2016

Degree Type

Dissertation

Degree Name

Doctor of Philosophy

Department

Engineering

First Advisor

John Boyland

Committee Members

Tian Zhao, Christine Cheng, Chris Hruska, Hong Yu

Keywords

Aliasing, Fractional Permissions, Linear Type, Mechanized Proof, Mutable State, Type System

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.

Download

Share

COinS