Typed intermediate languages and typed assembly languages for optimizing compilers require types to describe stack-allocated data. Previous type systems for stack data were either undecidable or did not treat arguments passed by reference. This paper presents a simple, sound, decidable type system expressive enough to support the Micro-CLI source language, including by-reference arguments. This type system safely expresses operations on aliased stack locations by using singleton pointers and a small subset of linear logic.

PDF file

In: International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO 07)

Details