HKU PL Group

We are a group of programming language researchers who study topics about functional language design, type theory, compilers and program analysis.
The University of Hong Kong

Polymorphic Subtyping and Dependent Types


The polymorphic subtyping relation, which captures the more-general-than relation between polymorphic and monomorphic types, is one of the main ways modern functional programming languages handles parametric polymorphisms (generic types) at higher rank. And with the trend of the rising dependently-typed languages, we explore the theoretical foundation of the combination of polymorphic subtyping and dependent types. In this talk, I will introduce both features and my current work of formal language design that puts them together, and my plan of going forward.