Paper notes: Toward a foundational typed assembly language

Title: Toward a foundational typed assembly language
PDF: 7b0f643010e5537ff02debab6b2fce4b.pdf

A paper from 2002 but a very interesting read; it formally defines a type system for a complete assembly language (TAL). The paper gives typing rules for the instructions and for memory allocation; its advantages are verification and reasoning (for things like heap object reachability) with machine-checked proofs.

An implementation (in OCaml) of TAL for x86 is TALx86; includes a type-checker and an assembler.

Original Twitter link: https://twitter.com/_argp/statuses/524588812731969536