diff --git a/docs/about/contributions.md b/docs/about/contributions.md new file mode 100644 index 0000000..686a257 --- /dev/null +++ b/docs/about/contributions.md @@ -0,0 +1,15 @@ +# 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... +