ν-types for Effects and Freshness Analysis

We define a type and effect system for a lambda-calculus extended with side effects, in the form of primitives for creating and accessing resources. The analysis correctly over-approximates the sequences of resource accesses performed by a program at run-time. To accurately analyse the binding between the creation of a resource and its accesses, our system exploits a new class of types. Our nu-types have the form nu N.tau |> H, where the names in N are bound both in the type tau and in the effect H, that represents the sequences of resource accesses.