It helps to ensure that complicated backend transformations such as the optimizations above as well as register allocation and more general instruction selection and scheduling are performed correctly. The type soundness of our assembly code implies many important security properties such as memory safety. As a result, our assembly code is a form of proof-carrying code . TAL applets, like Java applets, may be downloaded from untrusted sources on the internet, verified, and executed safely without fear they will corrupt the host machine. The present TAL effort has many applications in the security and compilation domains.
Future work involves compiling more expressive typed languages into the language of real machines.
We seek to reveal the connections between the typed lambda calculi which give semantics to many modern languages and the Von Neumann machines that implement them.