Type Checking Instructions
Key idea: register states
?={r1:t1, …, rn:tn}
"At this program point, register r1 has type t1, …, and register rn has type tn"
There is a type corresponding to register states
t ::= … code ? …
"Pointer to code whose entry point requires ?"