zbMATH — the first resource for mathematics

$$\nu$$-types for effects and freshness analysis. (English) Zbl 1250.68085
Leucker, Martin (ed.) et al., Theoretical aspects of computing – ICTAC 2009. 6th international colloquium, Kuala Lumpur, Malaysia, August 16–20, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-03465-7/pbk). Lecture Notes in Computer Science 5684, 80-95 (2009).
Summary: 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 \vartriangleright 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.
For the entire collection see [Zbl 1169.68004].

MSC:
 68N18 Functional programming and lambda calculus
Full Text: