CMU-CS-02-196
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-02-196

Toward a Foundational Typed Assembly Language

Karl Crary

December 2002

CMU-CS-02-196.ps
CMU-CS-02-196.pdf


Keywords: Typed assembly language, proof-carrying code


We present the design of a typed assembly language called TALT that supports heterogeneous tuples, disjoint sums, arrays, and a general account of addressing modes. TALT also implements the von Neumann model in which programs are stored in memory, and supports relative addressing. Type safety for execution and for garbage collection are shown by machine-checkable proofs. TALT is the first formalized typed assembly language to provide any of these features.

34 pages


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

This page maintained by reports@cs.cmu.edu