Foundational typed assembly language for grid computing

Abstract: "This report describes a type theory for certified code, called TALT-R, in which type safety guarantees cooperation with a mechanism to limit the CPU usage of untrusted code. At its core is the foundational typed assembly lanuage TALT, extended with an instruction-counting mechanism, or 'virtual clock', intended to bound the number of non-yielding instructions a program may execute in a row. The type theory also contains a form of dependent refinement that allows reasoning about integer values to be reflected in the typing of a program; in particular, the refinement system enables a simple but effective dynamic checking scheme for the clock, which we predict will greatly improve the performance of TALT-R programs. We exhibit a translation from a clock-ignorant source language into a form of TALT-R, demonstrating that the type system is expressive enough to write general programs in."