Show simple item record

dc.contributor.authorKabir, Ifaz 16:23:58 (GMT) 16:23:58 (GMT)
dc.description.abstractScala 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.en
dc.publisherUniversity of Waterlooen
dc.subjecttype safety, dependent object types, mutationen
dc.titleκDOT: A DOT Calculus with Mutation and Constructorsen
dc.typeMaster Thesisen
dc.pendingfalse R. Cheriton School of Computer Scienceen Scienceen of Waterlooen
uws-etd.degreeMaster of Mathematicsen
uws.contributor.advisorLhoták, Ondřej
uws.contributor.affiliation1Faculty of Mathematicsen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages