UWSpace is currently experiencing technical difficulties resulting from its recent migration to a new version of its software. These technical issues are not affecting the submission and browse features of the site. UWaterloo community members may continue submitting items to UWSpace. We apologize for the inconvenience, and are actively working to resolve these technical issues.
 

κDOT: A DOT Calculus with Mutation and Constructors

Thumbnail Image

Files

Kabir_Ifaz.pdf (490.21 KB)

Date

2018-09-26

Authors

Kabir, Ifaz

Journal Title

Journal ISSN

Volume Title

Publisher

University of Waterloo

Abstract

Scala is a functional and object-oriented programming language which unifies concepts from object and module systems by allowing for objects with type members which are referenced via path-dependent types. The Dependent Object Types (DOT) calculus of Amin et al. [2016] models only this core part of Scala, but does not have many fundamental features of Scala such as strict and mutable fields. Since the most commonly used field types in Scala are strict, the correspondence between DOT and Scala is too weak for us to meaningfully prove static analyses safe for Scala by proving them safe for DOT. This thesis presents the κDOT calculus, a calculus in the DOT family which supports mutable fields and constructors. κDOT can emulate both lazy and strict fields, and the constructor calls in κDOT emulate how objects are created in Scala. We present the key features of κDOT, the key ideas required for type safety, and discuss how the operational semantics of κDOT relates to that of Scala. κDOT is proven type safe via a mechanized proof in Coq.

Description

Keywords

type safety, dependent object types, mutation

LC Keywords

Citation

URI

http://hdl.handle.net/10012/13953

Collections

Theses
Computer Science