Campus Event Calendar
Event Entry
What and Who
Practical Semantic Foundations for Typed Assembly Languages
Andrew Appel
Princeton University, New Jersey
Informatik-Kolloquium
AG 1, AG 2, AG 3, AG 4, AG 5
Expert Audience
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 25 November 2005
15:30
-- Not specified --
45 - FR 6.2 (jetzt E1 3)
Hörsaal 002
Saarbrücken
Abstract
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]
Contact
--email hidden
passcode not visible
logged in users only
Veronika Weinand, 11/23/2005 12:39 -- Created document.