Summary: Gradual Featherweight Typestate
Roger Wolff¦ Ronald Garcia¦ ´Eric TanterX
July 2010 (Update December 2010)
School of Computer Science
Carnegie Mellon University
Pittsburgh, PA 15213
¦School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA
XPLEIAD Laboratory, Computer Science Department (DCC), University of Chile
Typestate oriented programming integrates notions of typestate directly into the semantics of an object-
oriented programming language. This document presents the formalization of Gradual Featherweight Type-
state, a typestate oriented language modeled after Featherweight Java. This language supports a classes-
as-states model of typestates, and utilizes a flow-sensitive type system for checking access permissions and
state guarantees, thereby enabling safe and modular typestate checking.
This research is supported by grants from the National Science Foundation and from IBM.
This work was supported by the National Science Foundation under Grant #0937060 to the Computing Research Association
for the CIFellows Project.
Keywords: gradual typing, hybrid types, access permissions, state guarantees