The SML-like module systems are small typed languages of their own. As is, one would expect a proof of their soundness following from a proof of subject reduction. Unfortunately, t...
We design and study νObj, a calculus and dependent type system for objects and classes which can have types as members. Type can be aliases, abstract types, or new types. The type...