SERVETTO M.

We show that a minimal subset of Java 8 excluding classes supports a simple and natural programming style, which we call lambda-based object-oriented programming. That is, on one hand the programmer can use tuples in place of objects (class instances), and tuples can be desugared to lambdas following their classical encoding in the...

We present a type and effect system for tracing and preventing sharing and mutation in imperative languages. That is, on one hand, the type system traces sharing possibly introduced by the evaluation of an expression, so that uniqueness and immutability properties can be easily detected. On the other hand, sharing and mutation can be prevented...

We present an imperative object calculus where types are annotated with qualifiers for aliasing and mutation control. There are two key novelties with respect to similar proposals. First, the type system is very expressive. Notably, it adopts the recovery approach, that is, using the type context to justify strengthening types, greatly...

We introduce a type and effect system, for an imperative object calculus, which infers sharing possibly introduced by the evaluation of an expression, represented as an equivalence relation among its free variables. This direct representation of sharing effects at the syntactic level allows us to express in a natural way, and to generalize,...