?

Log in

No account? Create an account
Fisher-Price: My First Invited Talk™ - Lindsey Kuper [entries|archive|friends|userinfo]
Lindsey Kuper

[ website | composition.al ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Fisher-Price: My First Invited Talk™ [Feb. 15th, 2011|12:30 pm]
Lindsey Kuper
[Tags|]

I just finished writing the abstract for my talk at Northeastern a week from tomorrow, which I'm also doing a dry run of at pl-wonks here on Friday.

Title: Parametric polymorphism through run-time sealing, or, theorems for low, low prices!

Abstract: Languages with parametric polymorphism provide the compile-time guarantee that programs behave uniformly regardless of the types they are instantiated with. In such languages, this parametricity guarantee forms the basis of data abstraction and makes possible Wadler's "theorems for free!" In this talk, I'll show how we can extend System F's parametricity guarantee to a Matthews-Findler-style multi-language system that combines System F with a Scheme-like language by use of dynamic sealing, which enforces data abstraction by using uniquely generated keys to seal values that should be kept opaque. While the use of sealing for this purpose has been suggested before, it has not previously been shown to preserve parametricity. Our proof employs a cross-language, step-indexed logical relation that uses possible worlds to capture the semantics of seal generation. Using this possible-worlds model, we can show two results: first, that System F's parametricity guarantee is preserved when interoperating with Scheme, and, second, that parametricity is preserved in a Scheme-only setting that interacts with System F only to implement a polymorphic contract system. (This talk describes current research being done in collaboration with Amal Ahmed and Jacob Matthews that expands on the work presented in their ESOP 2008 paper of the same title.)

Next things on to-do list:

  • Actually finish doing parametricity proof
  • Actually prepare talk (this time, heeding Matt Might's advice about not putting math on slides)

Every time I start trying to work on one of these things, I start panicking about the other not being done yet. Gonna have to do it by simultaneous induction.

LinkReply

Comments:
[User Picture]From: sstrickl
2011-02-17 05:20 am (UTC)
I am SO EXCITED! :D

Hopefully I will be happy fun Stevie and not a pitiful wreck while you are here*, because my thesis proposal is THE DAY BEFORE YOUR TALK.

(If you're going to be in town on Tuesday, you, of course, are invited. It's at 3 PM. I assume you'll be off doing family things or something if you're even here by then, so I do not expect you.)

* The former is almost certain, unless I don't get my ass in gear and FINISH MY SLIDES**. I've got a pretty nice outline for the talk, if I do say so myself, but that means nothing unless I convert it into a useful presentation aid. Well, unless I'm going to give the only proposal I've ever seen on the whiteboard, and... no, let's not and say we did.

** Sorry about the caps, I'm having random fits of mania interspersed with my inability to focus on slide-making.
(Reply) (Thread)
[User Picture]From: lindseykuper
2011-02-17 03:42 pm (UTC)
Aaaaaaaahhhhh thesis proposal! If I had known, I would have scheduled my flight so that I could be there for it! Alas, I don't get in until 5 p.m. on Tuesday.

Good luck! And FINISH YOUR DAMN SLIDES. I need to finish mine too! Slide-making party, tonight?
(Reply) (Parent) (Thread)
[User Picture]From: sstrickl
2011-02-17 04:43 pm (UTC)
Truthfully, I didn't have a firm date until middle of last week, so it probably wouldn't have helped. :)

Yessssss, that sounds like an excellent idea. LET US DO THIS.
(Reply) (Parent) (Thread)