?

Log in

No account? Create an account
ICFP 2010: A breathless recap - Lindsey Kuper [entries|archive|friends|userinfo]
Lindsey Kuper

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

ICFP 2010: A breathless recap [Sep. 30th, 2010|11:32 pm]
Lindsey Kuper
[Tags|]

I'm back in Bloomington after having spent the first part of this week at ICFP. This was my first time attending an academic conference, and it was great. I started making a list of all the awesome PL researchers and hackers I met at ICFP, but it got too long to put here. (Oh, the terrible problems I have.) So, here are just some highlights:

  • Derek Dreyer drew pictures of islands and worlds on graph paper for me;
  • I had a conversation with Benjamin Pierce on topics including but not limited to Schumann, kerning, dependent contracts, and Hello Kitty;
  • I got to have dinner with, and then draw a visual proof of the Pythagorean theorem on a napkin for, Chung-chieh Shan and Oleg Kiselyov; this "intuitive geometry" course I'm taking has officially justified its own existence, plus I got to hear Ken say, "Oh, you're that Lindsey!";
  • I also got to hear Mitch Wand say, "Oh, you're that Lindsey";
  • Nate Foster (whom I at first mistook for a student; oops!) actually inferred that I spent the summer working at GrammaTech, out of my idly mentioning that my summer internship was in Ithaca and located at the bottom of the hill;
  • Matt Might acknowledged my existence; okay, it was to make a joke at my expense when I spilled coffee on my pants, but it was an acknowledgment nonetheless;
  • I finally learned from Tim Chevalier how to pronounce "Chevalier";1
  • Rob simrob Simmons is just a joy of a human being;
  • I think I broke Jason jcreed Reed2 by telling him I have a twin sister;
  • Ron Garcia is the nicest person ever, and patiently listened to my story of How I Learned That Objects Are Good For Something After All;
  • Stevie sstrickl Strickland explained linear logic to me and introduced me to roughly five thousand Northeastern PLT people;
  • Dan Licata explained intensional types in an oh-is-that-all-it-means-sheesh-now-I-understand kind of way;
  • Chris chrisamaphone Martens graciously shared sleeping accommodations and running routes, and had the best hair at ICFP, as predicted, although Tim and Ron both got high marks in that category as well.

But enough of the interesting stuff. On to the boring stuff!

There were, of course, a lot of good paper presentations at ICFP. The two papers that seem to be the most closely related to the project I'm working on right now were "Logical Types for Untyped Languages", presented by Sam Tobin-Hochstadt from Northeastern, and "The Impact of Higher-Order State and Control Effects on Local Relational Reasoning", presented by Georg Neis from MPI-SWS. The latter in particular really blew my mind,3 and the former had a very nice quotation from a paper by Henglein and Rehof -- "Type testing predicates aggravate the loss of static type information" -- which is a nice, concise way of expressing what I've been trying to tell people.

In fact, after both of those talks had happened, it got much easier to explain my research to people who asked about it at the conference. Instead of having to synthesize my own elevator speech from scratch, I could just say something like, "We're working on the problem that Georg described, except swap out 'presence of call/cc' for 'presence of dynamically typed chunks of code scattered around inside statically typed code', and it's hard because of the problem that Sam described."

There were also a few talks that weren't particularly relevant to what I'm working on but which were very good. The "Lazy Tree Splitting" talk was great, because I actually understood all of it: I understood the premise, I understood the code samples, and I understood the authors' clever solution to the problem. I actually felt smarter at the end of the talk. And, of course, the "Play on Regular Expressions" was adorable, not to mention jaw-droppingly cool. When the video of the talk turns up, which I hope it does soon, everyone who teaches an undergrad automata theory course should show it to their students.


  1. I think next I'll work on being able to pronounce "Xavier Leroy".
  2. I think jcreed won ICFP. He scored a hat trick: he gave a well-received talk, was cited by name in one of the other talks, and was one of the co-winners of a prize (the Judges' Prize) in the ICFP Programming Contest. I'm pretty sure he was the only person to have accomplished all three this year.
  3. I think it's no coincidence, now that I look at the references, that this mind-blowing paper is also the only paper I've ever seen that cites both Dan and Amal.
LinkReply

Comments:
[User Picture]From: gwillen
2010-10-01 12:44 pm (UTC)
Hmm, maybe it's too bad I didn't go. I didn't want to miss more work after already missing a week for Burning Man, and it's not like I'm a PL researcher -- I'm just sort of a PL hobbyist. But it seems like I know a lot of people who went, and would have enjoyed a lot of the talks. Oh well. :-)

I finally learned from Tim Chevalier how to pronounce "Chevalier"
Shev'-al-yay?

I think jcreed won ICFP. He scored a hat trick: he gave a well-received talk, was cited by name in one of the other talks, and was one of the co-winners of a prize (the Judges' Prize) in the ICFP Programming Contest.
Haha, neat! What was he cited for?

the best hair at ICFP, as predicted
Hehehe.
(Reply) (Thread)
[User Picture]From: jcreed
2010-10-01 02:24 pm (UTC)
Karl mentioned my thesis in his "how to encode substructural logics in the Twelf you already have today"* talk.

*the solution is: you invent predicates that literally capture that such-and-such variable occurs linearly, and then every binding site has an extra proof obligation for that variable. The trouble is that while this works great for things like linearity (where the proper execution of the role of that variable (i.e. that it occurs just once) is independent of all the other variables around) we don't know how to do it for ordered logic, where the correct behavior of various variables is all interdependent. For this, at present, you need the big guns such as are described in my thesis.
(Reply) (Parent) (Thread)
[User Picture]From: lindseykuper
2010-10-01 02:33 pm (UTC)
Almost. Emphasis on the last syllable: shev-al-yay'. Rhymes with "hooray".
(Reply) (Parent) (Thread)
[User Picture]From: jcreed
2010-10-01 02:22 pm (UTC)
Re: Xavier Leroy: after that, try "Girard".

Ron Garcia just is the nicest person ever.

Also, the level of surprise I had at you having a twin was far below actual breakage! :)

Anyway, it was definitely nice to meet you. Woo conferences that go well!
(Reply) (Thread)
From: simrob
2010-10-01 08:27 pm (UTC)
And for the advanced level, Olivier Laurent. Which is particularly annoying because it has a perfectly reasonable pronunciation in Southern American English as AWW-LIVER, LAW-RENT.
(Reply) (Parent) (Thread)
[User Picture]From: jcreed
2010-10-02 02:01 am (UTC)
I feel pretty comfortable saying Leroy and Laurent. "Girard" fucks me up if I try to actually say it frenchily because of the two consecutive rs.
(Reply) (Parent) (Thread)
[User Picture]From: stereotype441
2010-10-01 02:27 pm (UTC)
Wow, now I really wish I had gone.

Also thanks for mentioning "Logical Types for Untyped Languages". The paper is online and it sounds like it's probably right up my alley. I'm going to read it over breakfast this morning.

I miss you, Lindsey, and I'm excited to see what a phenomenal CS education you're getting!
(Reply) (Thread)
[User Picture]From: lindseykuper
2010-10-01 02:59 pm (UTC)
I didn't know you were considering going! I'd have loved to see you there. The next one will be in Tokyo (!) in November 2011 -- put it on your calendar and think about it!
(Reply) (Parent) (Thread)
[User Picture]From: sonetka
2010-10-01 03:54 pm (UTC)
Hey, Matt Might! He lived across the street from us in Salt Lake; his wife and I are friends. I'm glad he acknowledged your existence :).
(Reply) (Thread)
[User Picture]From: lindseykuper
2010-10-01 04:15 pm (UTC)
Oh, cool. If I manage to meet him at some other conference sometime, I will give your regards to him!
(Reply) (Parent) (Thread)
[User Picture]From: tim.dreamwidth.org
2010-10-01 05:50 pm (UTC)
At the Eugene summer school, Greg Morrissett introduced Xavier Leroy by saying something like "and a guy from Tennessee could never possibly hope to pronounce his name, so I won't try." I thought Xavier should have, later on, introduced Greg by saying "and a guy from France could never possibly hope to pronounce his name," but he didn't.
(Reply) (Thread)
[User Picture]From: lindseykuper
2010-10-01 07:51 pm (UTC)
Heh. I think Europeans have figured out that most of us Amurricans like hearing European pronunciations of our names. Doug Hofstadter told us that he didn't like to be called "Douglas" except in France, where people said doog-lahs' which was great.
(Reply) (Parent) (Thread)
From: simrob
2010-10-01 08:22 pm (UTC)
Hey aww that's nice and it was terrific to meet you as well. This was a week full of Meeting People From The Internet.
(Reply) (Thread)