Toward a foundational typed assembly language

We present the design of a typed assembly language called TALT that supports heterogeneous tuples, disjoint sums, 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. Categories and Subject Descriptors D.3 [Programming Languages]: Language Constructs and Features; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs. General Terms Languages, Security, Verification Keywords Typed assembly language, proof-carrying code

• Type: Conference
• Year: 2003
• Where: POPL
• Authors: Karl Crary
• Keywords: General Terms Languages, POPL 2003, Programming Languages, Typed Assembly Language, Von Neumann Model