AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

Expert Audience

English

60 Minutes

Saarbrücken

Type refinements, introduced by Freeman and Pfenning and explored by
Davies and Dunfield, unify the ontological and epistemic views of typing.
Types tell us what programming language constructs exist, whereas refinements
express properties of the values of a type.  Here we show that refinements are
very useful in compiler correctness proofs, wherein it often arises that two
expressions that are inequivalent in general are equivalent in the particular
context in which they occur.  Refinements serve to restrict the contexts
sufficiently so that the desired equivalence holds.  For example, an
expression might be replaced by a more efficient one, even though it is not
generally equivalent to the original, but is interchangeable in any context
satisfying a specified refinement of the type of those expressions.

We study here in detail a particular problem of compiler correctness, namely
the correctness of compiling polymorphism (generics) to dynamic types by
treating values of variable type as values of a universal dynamic type.
Although this technique is widely used (for example, to compile Java
generics), no proof of its correctness has been given to date.  Surprisingly,
standard arguments based on logical relations do not suffice, precisely
because it is necessary to record deeper invariants about the compiled code
than is expressible in their types alone.  We show that refinements provide an
elegant solution to this problem by capturing the required invariants so that
a critical invertibility property that is false is general can be proved to
hold in the contexts that arise in the translated code.  This proof not only
establishes the correctness of this compilation method, but also exemplifies
the importance of refinements for compiler correctness proofs more generally

Brigitta Hansen

0681 93039102

--email hidden

Yes

Kaiserslautern

G26

112

passcode not visible

logged in users only