Igarashi and Kobayashi have proposed a general type system for
checking whether resources such as files and memory are accessed in
a valid manner. Their type system is, however, for
call-by-value lambda-calculus with resource primitives, and
does not deal with non-functional primitives such as exceptions and
We extend their type system to deal with exception primitives and prove
soundness of the type system.
Dealing with exception primitives is especially important in practice,
since many resource access primitives may raise exceptions.
The extension is non-trivial: While Igarashi and Kobayashi's type
system is based on linear types, our new type system is a combination of
linear types and effect systems.
We also report on a prototype analyzer based on the
new type system.