A little over two weeks ago, I set out on a trip to Copenhagen to attend ICFP 2012 and affiliated events. I was nervous. Aside from being my first trip to a conference abroad, it was my first trip to northern Europe at all, and my colleague and travel companion Chris chrisamaphone and I had decided to make an oven char1 out of it by scheduling our flight home for five days after the conference ended, with little idea of where we'd go or what we'd do for the extra five days. I wasn't nervous about any of those things, though -- I was nervous because the author response period for POPL was to overlap directly with ICFP, which meant that on the first day of ICFP, my advisor Ryan and I would receive the reviews for our POPL submission.
Like many conferences, POPL uses a system in which paper submissions go through an initial round of reviews that end in recommendations for acceptance or rejection, but no final decision. The authors then have a brief window of time -- four days, in the case of POPL this year -- to respond to those reviews, and their responses go back to the conference program committee to make final decisions about which papers to accept. Author response is a double-edged sword: it's time-consuming and stressful -- who wants to have to write a response, after already having busted one's butt to write the paper in the first place? -- but it's also nice to have the opportunity to address issues raised in the reviews, and perhaps correct any misconceptions the reviewers may have had. Moreover, it means that the review process is a little more like a conversation between authors and reviewers than it would be otherwise. In most fields other than CS, the top publishing venues are journals rather than conferences. The "conversation" aspect of journal publishing, in which authors and reviewers might go back and forth several times until a paper is ready to publish, is one of the things that non-CS fields enjoy in their top venues, and having author response as part of the conference review process in CS is, it seems to me, a way of retaining a little of that. (Of course, we could also retain it by reviving CS journals, but that's a blog post for another time.)
For Ryan and me, our POPL submission was the first submission of the first paper of a new line of work on lattice-based deterministic parallelism, and I was worried about all kinds of things: that the reviewers would poke a hole in our proof of determinism, or that they'd point out that our formalism was originally proposed in [Tarjan, 1985], or that, worst of all, they'd just find the whole thing to be uninteresting. On the other hand, it was, well, the first submission of the first paper of a new line of work, and after several months of working on it, I was excited to finally find out what reviewers thought!
Once my connecting flight arrived in Toronto, I met up with Will, Dan, and Chris, since it turned out we were all sharing a flight to Copenhagen. We arrived at CPH on Saturday morning, giving us a chance to adjust to local time before the pre-conference workshops the next day -- especially important for Chris, because she was going to be speaking at LFMTP.
I really liked all the talks I saw on Sunday. At LFMTP, there were two great invited talks: Rob simrob's "Walk in the
Substructural Park" tour of substructural operational semantics, and Stephanie Weirich's candid look at where the
last seven years of mechanized metatheory have gotten us as a field. I also liked seeing Chris present her LF in LF project,
which I might not have
understood much of except that Rob and I had seen
her practice talk the evening before, which had given me a chance to get all my n00b questions, like "What does 'eta-long' mean?", out of the way in advance.
At the HOPE workshop, which I'd been looking forward to for months, I got to see Jamie talk about the work he's been doing
with Amal on open verified compilation.
Usually, compiler correctness proofs work by specifying a relationship between source programs and target programs, then proving that the compiler preserves that relationship. But such proofs assume that one source language is compiled to one target language, when in reality, an executable might be cobbled together from source files written in various languages, plus precompiled libraries.
So, for the proof technique to work, we need a single source-level program in a single language that corresponds to this target-level mishmash o' stuff; how do we come up with one of those? Amal
and Jamie had the idea of using a Matthews-Findler-style
multi-language semantics, using boundary terms to wrap target-level
terms in source-level wrappers and vice versa, making it possible to
give a source-level semantics to target-level terms.
The same idea allows for reasoning about multi-pass compilation, because
if the compiler has several ILs, a target term can be wrapped in
nested boundary terms, one for each adjacent pair of ILs, to get a a term in a higher-level IL or a
source term, whichever is needed. It's a simple idea, but not one that I think had been
thought of before -- other applications of boundary terms that I've seen
have all been about relating languages that are different (say, typed and
untyped) in some way, but usually at the same level of abstraction, whereas I think this is the first work I've seen that uses boundary terms to reason about compilation. So, that was pretty cool. There were lots of afternoon talks at HOPE that looked interesting, but I missed almost all of them, including one by Aaron Turon that I really would've liked to have seen, because I was over at LFMTP listening to
Stephanie and Chris. I was able to get back in time for the last session of HOPE, though,
where Uday Reddy closed out the day with a thought-provoking talk on
ICFP proper began on Monday with Conor McBride's keynote talk, which did not disappoint: it involved a costume change and a live demo of Agda. In the next session, Neel neelk Krishnaswami presented his paper, "Superficially Substructural Types", on a substructural type system for reasoning about user-defined notions of logical resources. Not gonna lie: the main thing I remember about the talk is Neel's incredibly calm, tranquil voice. It was like this at POPL in January, too -- somehow he manages to be enthusiastic without being bouncy and manic. How do you do that, Neel?
Around noon on Monday, Ryan and I got our POPL reviews. Some of my worries, it turned out, were unfounded: the reviewers didn't find fault with our proof, they didn't point out related work that we missed, and they thought our idea was interesting. Yay! Rather, their main complaints were that we need to motivate the paper better and provide more real-world examples of why a new approach to deterministic concurrency is called for. I think that those are fair points: we need to give more examples of programs that are more easily expressible with a monotonic-multiple-assignment language than with a single-assignment language or another existing model. I spent a lot of time thinking about that for the rest of the conference, unfortunately compromising my ability to focus on the talks. Of course, Ryan and I were far from the only people at ICFP who were in the working-on-POPL-responses boat. There's a lot of overlap between the ICFP and POPL communities, and I noticed lots of other people skipping talks, especially near the end of ICFP -- a raw deal for the folks who were scheduled to speak then! I can't say that the overlap was all bad, though, because working on our response during ICFP meant that the high-level aspects of my research were fresh in my mind while chatting with other researchers, leading to some good hallway conversations that I'm in the process of following up on now.
Despite the distraction of the POPL response period, I did manage to see some great talks on Tuesday and Wednesday. On Tuesday, I liked Lee Pike's talk on DIY high-assurance compilers, which began with an explanation of the DIY movement, and I thought José Pedro Magalhães's talk on adding deferred type checking to Haskell was great despite
the joking, dismissive introduction it got from the session chair.
There was some drama on Tuesday afternoon: I was sitting and talking with Ryan when my colleague Adam -- who was
scheduled to speak a short while later about the paper he co-authored
with Ryan and various other IU folks -- came hurrying up to us and announced, "I have
clothes!" I didn't know what he was talking about, but I didn't question it; after all, he wasn't wrong. It was only later, after the successful completion of his talk, that Adam explained: Delta had lost his suitcase, so he'd had to go
shopping for clothes to wear for the talk -- in Copenhagen, on foot, in the rain -- with only a few hours to spare. Somehow, he'd managed
to find and purchase new clothes with enough time left over to give a practice
talk to Ryan, Jamie, and me. As it turned out, Adam's talk kicked off the "Parallelism" session, but all the talks in the session were
so similarly themed that it probably wouldn't have been inaccurate to just name
the session "Programming GPUs with Functional Languages". I had my
ears pricked for any mention of IVars, but Adam's talk was the only
one of the three where they came up. Still, I got a lot out of the
session; I thought Lars Bergstrom's talk, on nested data parallelism on GPUs, was particularly well-delivered. Chris commented afterward that
she felt she understood what was going on in the session despite it
not being her area at all, so that speaks highly of all the presenters.
My talk attendance on Wednesday was especially spotty: I only saw three
talks, because I was furiously working to finish up our author
response. The three talks I picked were winners, though: I saw Peter
Sewell's entertaining "Tales from the Jungle" keynote, Phil Wadler's
"Propositions as Sessions" (featuring the second high-profile costume
change of the conference, by my count), and Matt Might's whiz-bangy
talk on introspective pushdown analysis of higher-order programs. Wednesday concluded with a canal cruise and a falafel pilgrimage led by David, a local whom I'd met at OPLSS over the summer. And that was ICFP!
Although this was my first conference abroad and my first
time in northern Europe (and only my second time in Europe at all, after Alex's and my Barcelona trip last year), I found the travel experience to be stunningly easy and fun. Nobody fingerprinted and photographed me at customs (like in Japan in 20082), and nobody introduced themselves to me by seizing me and kissing my cheeks (like in Spain last year; it was the local custom, of course, but I was unprepared for it). Almost everyone we encountered spoke
fluent English, making things a lot easier for my monoglot American
self, although I did pick up a couple of Danish words by the end of
the trip. It was easy to get around: good public transportation and an
impressive amount of bike infrastructure. Finally, there were ample opportunities for nerding out about Danish design -- Chris' and my room at the
conference hotel looked like something out of an Ikea catalog.
It also featured a Piet Hein poem on the wall that I hadn't seen before.
En tanke i martssolen.
Kultur - det er ikke en fin menuet,
i en fortids-frednings-forening,
men det at man slås for sin modstanders ret
til at slås for den modsatte mening.
Translated, with machine assist:
A thought in the March sun.
Culture -- it is not a fine minuet,
in a past-preservation association,
but the fight for one's opponent's right
to fight for the opposite position.
Chris was a fantastic travel companion. Not
only did she make all our hotel arrangements in Copenhagen, she also took charge of planning the second half of our trip. We ended up heading to Aarhus, about a three-hour train ride away from Copenhagen, where we spent Thursday through Sunday staying with her friend Ian and his wife Anna. Although this part of the trip was mostly vacation, Ian also arranged for us both to give talks on Friday to the PL group at Aarhus University, where he's a Ph.D. student. Chris
gave her LFMTP talk, and I quickly put together an abbreviated version of the talk I gave at Berkeley last month. Our visit was brief, but I really enjoyed it -- it's always interesting to visit other groups, hear about what they're working on, and share my own work. And I'm totally stealing this idea for my own research group!
Ian and Anna were fantastic, too, cooking for us on the first night of our visit and teaching us the top-secret European technique for quick duvet cover application. For the weekend, they went off on an adventure of their own, so we had their adorable apartment to ourselves for a couple of days.
Aside from the fun of getting to meet and spend time with Ian and Anna, I think
it added a lot to our trip to be able to have the Authentic Danish
Experience™ of staying in their apartment, shopping at the local
stores, and cooking for ourselves, instead of only staying in hotels
and eating in restaurants as we'd done in Copenhagen. It was also great to
have a couple of days to unwind in Aarhus, after all the crowds and
noise of ICFP and the stress of the author response period. We went running, visited the
beautiful art museum in Aarhus, and even tried out some free public
bikes, which was fun even though the bikes themselves were pretty
bad. On Sunday, we headed back to Copenhagen on the train and spent the last night of our trip in a hostel that Rob had recommended, before finally heading home on Monday.
I had a great time in Denmark, but I'm left feeling a bit envious of all the people I know who had papers to present at the
conference or at the affiliated workshops. It's great to keep talking about my work -- I think the talk
I've been giving gets a little better every time -- but I'm impatient to get the the first paper published and move on to the next stage
of the work. As Dan pointed out in my
first year of grad school, ting tager tid.