Andrew Appel

"Practical Semantic Foundations for Typed Assembly Languages"

(Gemeinsames Kolloquium der TU-Kaiserslautern und der Universität des Saarlandes)

We have completed the machine-checked semantic soundness proof of a rich specification language, Typed Machine Language (TML). We prove type soundness of TML using syntactic logical relations encoded in pure higher-order logic, and therefore our soundness proof is checkable in a tiny proof checker. TML is useful for proving soundness of Typed Assembly Languages, as we demonstrate by using TML to construct the semantics for LTAL, the low-level typed assembly language that is the output of our core-ML-to-Sparc compiler.

In TML we provide the first semantic model for a type system with updatable references to values of impredicative quantified types. Both impredicative polymorphism and mutable references are essential when representing function closures in compilers with typed closure conversion or when compiling objects to simpler typed primitives.

We also present a compositional instruction calculus that makes the connection between von Neumann machine semantics and low-level type systems.

Joint work with A. Ahmed, C.R. Richards, K.N. Swadi, G. Tan, D. Wang