Programming Languages

Algebraic Subtyping for Ouroboro

Assigned to Justus Springer.

Algebraic subtyping is a new approach which unifies parametric polymorphism, subtyping and complete type inference with principal types. The presentations used in the literature illustrate the approach by considering systems with function types, record types and base types, since these form a minimal type theory which allows to illustrate contravariance (function types) and subtyping (record types).

Algebraic subtyping is a very natural fit for a system which only contains extensible data and codata types, since these subsume function types, record types, ordinary data types and many more.

The thesis consists in applying and extending the algebraic subtyping approach to a structural version of the Ouroboro type theory.

Further Information

Contact

David Binder

Ingo Skupin