[Pl-seminar] Semantics Seminar Schedule

Mitchell Wand wand at ccs.neu.edu
Wed Jul 25 00:05:02 EDT 2007

NU Programming Languages Seminar
Wednesday, 7/25/07
Room 166 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Jacob Matthews
University of Chicago

Parametricity from Run-Time Sealing

In this talk, I will follow up on my earlier talk "Operational
Semantics for Multi-Language Programs" by extending the technique I
presented there to an embedding of call-by-value System F and the
call-by-value untyped lambda calculus. While it is not hard to build a
type-sound embedding between those two languages, it turns out to be
somewhat more challenging to devise an embedding that preserves
Reynolds' parametricity property, i.e. that a value whose type
contains a free variable must be completely indifferent to the set of
values chosen to be the interpretation of that variable. I use
Morris's notion of dynamic seals to give such an embedding, and show
that the System F side of the resulting system retains parametricity.
I will not assume familiarity with the formal details of
parametricity; instead I will devote a section of the talk to
introducing them (and, more generally, the method of logical

Upcoming Events:

# Don't you want to speak at pl-seminar?


More information about the pl-seminar mailing list