We define a type and effect system for a λ-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 ν-types have the form νN. τ̇τ &rtri H, where the names in N are bound both in the type τ and in the effect H, that represents the sequences of resource accesses. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Bartoletti, M., Degano, P., Ferrari, G. L., & Zunino, R. (2009). ν-Types for effects and freshness analysis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5684 LNCS, pp. 80–95). https://doi.org/10.1007/978-3-642-03466-4_5
Mendeley helps you to discover research relevant for your work.