Computer Science Department
School of Computer Science, Carnegie Mellon University


Nominal Wyvern: Employing Semantic Separation for Usability

Yu Xiang Zhu

M.S. Thesis

April 2019


Keywords: Nominality, Wyvern, Dependent Object Types, Subtype Decidability

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 subtypingbased 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, NominalWyvern 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.

91 pages

Thesis Committee:
Jonathan Aldrich (Chair)
Heather Miller
Alex Potanin (Victoria University of Wellington, NZ)

Srinivasan Seshan, Head, Computer Science Department
Tom M. Mitchell, Interim Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by