15 lines
775 B
Markdown
15 lines
775 B
Markdown
# Contributions
|
|
|
|
* We introduce a type system able to express predicated types, a unified way to
|
|
express existance of method- and traits depending on some predicate on the
|
|
subtyping relation.
|
|
* We define our subtyping relation as a natural extension to type systems based
|
|
on semantic subtyping.
|
|
* We express our subtyping using a novel approach based on the sequent calculus.
|
|
* We show the correctness of our subtyping relation and type system.
|
|
* We explain how this type system may be used to succinctly describe programs
|
|
involving for example capabilities and constructions such as type classes.
|
|
* We have implemented the type system and give examples of how its use
|
|
simplifies expressing many properties in object oriented languages, including
|
|
things like...
|
|
|