[PRL] Fwd: Possible visit

[Mitchell Wand]

Hi guys--  Jacob Matthews will be in town from 7/25 to 8/1 (that's Wed thru
Wed).   Are some days better than others for scheduling his talk?

--Mitch

---------- Forwarded message ----------
From: Jacob Matthews <jacobm at cs.uchicago.edu>
Date: Jun 7, 2007 5:05 PM
Subject: Possible visit
To: Matthias Felleisen <matthias at ccs.neu.edu>, wand at ccs.neu.edu
Cc: Robby Findler <robby at cs.uchicago.edu>

Hi Matthias, Mitch ---

I'm going to be in Massachusetts at the end of July (probably around
the 25th), and I've been wanting to give another talk at NEU and to
get your insights on a hard problem related to the multi-language work
I've been doing lately. If I were to push back my flight by a week,
could I camp out at NEU, give a talk and have meetings with either or
both of you and anyone else who might have insight?

The talk would be a sequel to the Earth vs. Mars talk I gave last time
--- I can talk about polymorphism and a proof I've recently completed
(but haven't yet had peer reviewed!) that dynamic sealing suffices to
ensure parametricity when a typed, parametric language allows untyped
functions to be imported at polymorphic types; or I can talk about how
to embed call-by-name with call-by-value and the equational problems
that arise there; or both.

What I'd like to pick your brains about is about those equational
problems that arise. I'd like to come up with a proof technique for
establishing that if e_1 =L1 e_2 in call-by-name, then e_1 =L1+L2 e_2,
where =L1 is contextual equivalence in some language L1,  =L1+L2 is
contextual equivalence in a multi-language system that combines
languages L1 and L2, and e_1 and e_2 re both completely L1 terms. In
particular I'd like to prove this where L1 is an simply-typed
call-by-name lambda calculus, L2 is an simply-typed call-by-value
lambda calculus, and the embedding is a slightly subtle one that
avoids introducing strictness points around boundaries (this is a
little trickier than it may sound but certainly doable).

I have tried logical relations; when I did I ran into a huge snag. The
snag may be fixable, in which case I think my logical relation may go
through; otherwise a bisimulation argument might also work, but I
don't know how to do sophisticated bisimulations at all. So, I think
it would be very fruitful for me to work with people who actually know
what they're talking about when it comes to equational reasoning :)

So does my plan to visit sound workable? Will people even be around in
the middle of the summer to talk to me or hear me talk?

Thanks!
-jacob
-------------- next part --------------
HTML attachment scrubbed and removed