Reference1:
Statically typed intermediate languages are effective tools for staging the compilation of high-level languages. Types express invariants that help programmers understand their programs, and strongly typed languages prevent many common programming errors. Compiler writers can use these properties to debug sophisticated program transformations such as closure conversion and optimizations like datatype specialization. Furthermore, types not only help check the correctness of transformations but enable analyses or optimizations that are extremely difficult without them.
The goal of the TAL project is to extend the paradigm of type-directed compilation to its limit. We compile high-level languages that include features such as higher-order polymorphic functions, datatypes, modules, objects, and subtyping into a series of typed intermediate languages and finally into a Typed Assembly Language (TAL). Unlike any other compiler, we not only use typed intermediate languages but also typed target languages.
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.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?