A generic type-and-effect system

11 years 1 months ago
A generic type-and-effect system
Type-and-effect systems are a natural approach for statically reasoning about a program’s execution. They have been used to track a variety of computational effects, for example memory manipulation, exceptions, and locking. However, each type-and-effect system is typically implemented as its own monolithic type system that hard-codes a particular syntax of effects along with particular rules to track and control those effects. We present a generic type-and-effect system, which is parameterized by the syntax of effects to track and by two functions that together specify the effect discipline to be statically enforced. We describe how a standard form of type soundness is ensured by requiring these two functions to obey a few natural monotonicity requirements. We demonstrate that several effect systems from the literature can be viewed as instantiations of our generic type system. Finally, we describe the implementation of our type-and-effect system and mechanically checked type soundn...
Daniel Marino, Todd D. Millstein
Added 17 Mar 2010
Updated 17 Mar 2010
Type Conference
Year 2009
Where TLDI
Authors Daniel Marino, Todd D. Millstein
Comments (0)