Tuesday, April 30, 2019 - 2:30pm
Location:200 Elliot Dunlap Smith Hall
Speaker:YU XIANG (BILLY) ZHU, Masters Student https://www.andrew.cmu.edu/user/yuxiangz
Nominal Wyvern: Employing Semantic Separation for Usability
This thesis presents Nominal Wyvern, a nominal type system that emphasizes semantic separation for better usability. Nominal Wyvern is based on the dependent object types (DOT) calculus, which provides greater expressivity than traditional object-oriented languages by incorporating concepts from functional languages. Although DOT is generally perceived to be nominal due to its path-dependent types, it is still a mostly structural system and relies on the free construction of types. This can present usability issues in a subtyping-based system where the semantics of a type are as important as its syntactic structure. Nominal Wyvern overcomes this problem by semantically separating structural type/subtype definitions from ad hoc type refinements and type bound declarations. In doing so, Nominal Wyvern is also able to overcome the subtype undecidability problem of DOT by adopting a semantics-based separation between types responsible for recursive subtype definitions and types that represent concrete data. The result is a more intuitive type system that achieves nominality and decidability while maintaining the expressiveness of f-bounded polymorphism that is used in practice.
Jonathan Aldrich (Chair)
Alex Potanin (Victoria University of Wellington)