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.
 

Context-Sensitive Optional Type Systems Meet Generics: A Uniform Treatment and Formalization

Thumbnail Image

Files

Shi_Haifeng.pdf (593.69 KB)

Date

2023-12-14

Authors

Shi, Haifeng

Journal Title

Journal ISSN

Volume Title

Publisher

University of Waterloo

Abstract

This thesis explores a novel design of context-sensitive optional type systems which supports generics. Optional type systems, as the name suggests, optionally enforce type rules in typechecking and can be switched on only when needed. They give flexibility to developers because, whenever they need optional type properties, they can plug these properties into the compiler and perform additional rounds of semantic analyses. Context-sensitive type systems help to resolve a declared type to different types according to usage contexts. Type parameters and type variable uses can be annotated with optional type qualifiers, and these type qualifiers can impact the process of type argument substitution and context-sensitive resolution of types. This thesis shows (1) existing optional type systems either do not support generics or have type safety issues when context sensitivity is involved; (2) type variables and monomorphic types are treated differently in the type check and type inference modes by these type systems. This thesis formalizes a Java-like language, introduces a new qualifier Sub to clarify the semantics of unannotated type variables, and presents a new viewpoint adaptation rule to model how context-sensitive type systems interact with generics. As a concrete instantiation, a case study is conducted in a context-sensitive type system called Practical Immutability for Classes and Objects (PICO). PICO offers reference and object immutability to Java, making Java programs more robust in areas like thread-safe programming and aliasing control. This thesis also gives an overview of PICO, identifies some interesting issues, and fixes them. Last, this thesis formalizes the core parts of non-generic version of PICO, providing the well-formedness rules, type rules, and operational semantics.

Description

Keywords

Optional Type System, Generics, Immutability

LC Keywords

Citation

URI

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

Collections

Theses
Electrical and Computer Engineering