Abstract. There is a growing need to provide low-overhead softwarebased protection mechanisms to protect against malicious or untrusted code. Type-based approaches such as proof-ca...
abstractions, such as closures, tuples, and user-defined abstract data types. The type system ensures that well-typed programs cannot violate these abstractions. In addition, the ...
J. Gregory Morrisett, David Walker, Karl Crary, Ne...
Typed assembly languages provide a way to generate machinecheckable safety proofs for machine-language programs. But the soundness proofs of most existing typed assembly languages...
Typed Assembly Languages (TALs) can be used to validate the safety of assembly-language programs. However, typing rules are usually trusted as axioms. In this paper, we show how to...
Gang Tan, Andrew W. Appel, Kedar N. Swadi, Dinghao...
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 t...