thesis_access.pdf (553.29 kB)
Download file

Ownership and Immutability in Coq

Download (553.29 kB)
posted on 2021-12-08, 10:39 authored by Mackay, Julian

A significant issue in modern programming languages is unsafe aliasing. Modern type systems have attempted to address this in two prominent ways; immutability and ownership, and often a combination of the two [4][17]. The goal of this thesis is to formalise Immutability and Ownership using the Coq Proof Assistant, a formal proof management system [13]. We encode three type systems using Coq; Featherweight Immutable Java, Featherweight Generic Java and Featherweight Ownership Generic Java, and prove them sound. We describe the challenges presented in encoding immutability, ownership and type systems in general in Coq.


Copyright Date


Date of Award



Te Herenga Waka—Victoria University of Wellington

Rights License

Author Retains Copyright

Degree Discipline

Computer Science

Degree Grantor

Te Herenga Waka—Victoria University of Wellington

Degree Level


Degree Name

Master of Science

ANZSRC Type Of Activity code

970108 Expanding Knowledhe in the Information and Computing Sciences

Victoria University of Wellington Item Type

Awarded Research Masters Thesis



Victoria University of Wellington School

School of Engineering and Computer Science


Potanin, Alex; Groves, Lindsay