EnerJ: Approximate Data Types for Safe and General Low Power Computation—Full Proofs

This section introduces the core type system, which is made up of type qualifiers that extend Featherweight Java [1]. Section 2 describes the big-step operational semantics that define the language’s runtime system. Section 3 proves a number of properties about the language, the most important of which is non-interference (intuitively, that the precise part of the program is unaffected by the approximate part). The appendices contain complete listings, generated by the Ott tool, of the language’s grammar and definitions. 1