Computer Science Department
School of Computer Science, Carnegie Mellon University


Foundational Typed Assembly Language for Grid Computing

Joseph C. Vanderwaart, Karl Crary

Feburary 2004

Keywords: Certified code, type theory, typed assembly language, distributed computing, resource bound certification.

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 language 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.

62 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by