thesis_access.pdf (553.29 kB)
Download file

Ownership and Immutability in Coq

Download (553.29 kB)
thesis
posted on 08.12.2021, 10:39 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.

History

Copyright Date

01/01/2013

Date of Award

01/01/2013

Publisher

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

Masters

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

Language

en_NZ

Victoria University of Wellington School

School of Engineering and Computer Science

Advisors

Potanin, Alex; Groves, Lindsay