Campus Event Calendar

Event Entry

New for: D1, D2, D3, D4, D5

What and Who

Type Refinements for Compiler Correctness

Robert Harper
Carnegie Mellon University
SWS Colloquium
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI  
Expert Audience

Date, Time and Location

Thursday, 22 August 2013
60 Minutes
E1 5


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

Video Broadcast

passcode not visible
logged in users only

Brigitta Hansen, 08/22/2013 10:49
Brigitta Hansen, 08/21/2013 10:41 -- Created document.