I'm back in Mountain View, living at the same apartment complex, working at the same place with the same people, waiting at the same traffic lights on my way to and from work. Even the dented PLDI water bottle that I left in the kitchen cabinet at the office was still there after nine months.¹

If I'm lucky, I might even manage to convince myself that I'm qualified for, and capable of, doing my job, on account of having literally done it before.

Until my husband reminded me a couple weeks ago, I hadn't thought about the fact that I'd need a passport to go to Toronto.¹ My passport expired in January. So on Wednesday, I drove the four and a half hours to Chicago, the nearest city with a regional passport agency, to get an expedited passport renewal.

Actually, Wednesday wasn't the first time I've made that trip for that reason; we also did it last winter when my husband was about to fly to Israel. So, although I was by myself this time, I already knew the drill. It goes like this: after your four-and-a-half-hour drive, you park somewhere around State and Roosevelt. You feed the "PAY TO PARK" machine ($10.50 for three hours). You find a Walgreens and pay to have an unflattering passport photo taken by a sullen clerk. You forgot to eat breakfast and must resist the urge to buy horrible candy at Walgreens.

You walk up State Street and turn left on Jackson to get to the Kluczynski Federal Building, a Mies van der Rohe skyscraper done in black with black as an accent color. Because you're not allowed to show up early, you stop at Intelligentsia Coffee across the street, and you're pleasantly surprised by the little red star at the bottom of your coffee cup that you always forget is going to be there. You fidget nervously while waiting to go through the metal detector, because the line is moving slowly and you're not allowed to show up late, either.

(You also meet up with your sister for an hour at the coffee shop, and that's really nice, but you're leaving that part out of the story, because you're going for a bleak vibe here.)

You ride the elevator up to the 18th floor, where you are told that you must turn off your phone before entering the passport office. You do so, and enter. You stand in line, again, while an electronic sign helpfully informs you that there is a "WAIT TIME: 0 MIN", and you mutter to the guy in line next to you, who is wearing a Linux cheat shirt and therefore might appreciate your sense of humor, that if the wait time were really zero minutes then we wouldn't be waiting right now.

You realize that everyone in the line but you is clutching an already-filled-out form, and that the blank forms are over by the wall. You duck out of line and go to fill out a form. You quickly realize that in order to fill out the form, you need information that is only available on your phone. You try to stand in such a way that no one will see you turning on your phone, which takes forever to boot up because it's a goddamn G1 from 2008. You fill out the form as hastily as possible and return to line.

On the other side of the room is the door to the "interview" room. Next to that door, there's an official-looking sign on the wall with a single word on it in all caps. It's something kind of scary-sounding. Like "SILENCE". Or "CONTEMPT". Except not either of those. But you can't take a picture of it, because you're not allowed to use your phone, so you'll forget what it says a few minutes after leaving, even though you exhort yourself not to forget, and nobody's ever going to believe you.

You request a 24-page book, because that's what your 2002-2012 passport had been, and you used only two of those pages. But the agent upsells you to the 52-page book. Maybe you'll travel a lot more in your 30s than you did in your 20s.

You pay the $170 expedited-passport fee. (The woman at the next window over complains about the fee because "a passport should be a human right". A few minutes later, she's flirting with the passport agent.) You're told to return in an hour for your new passport.

You walk back to State and Roosevelt and feed the parking meter. You order a salad at Panera. Green gargoyles leer at you from the top of the public library.

After sixty minutes, plus ten for good measure, you go back to the Kluczynski Building. You wait in another room this time. A little boy is excited to get his passport and go to Mexico.

When your number is called, you receive a blue envelope containing your old and new passports. Your old passport now has two holes punched through the cover. Your new one is twice as thick and has a sturdier cover. You are told to look over it for mistakes. (You wonder how long you'd have to wait to have a mistake fixed if you found one.) You realize that the new photo really isn't so bad, at least not compared to the previous one, which was taken when you were 19 and had a rather rounder face and a rather worse haircut and evidently believed that yellow plastic barrettes and heavily plucked eyebrows looked good on you.

You make the four-and-a-half-hour drive back home with your new passport. The weather is perfect. As you're crossing the state line, a cheesy country song on the radio actually makes you tear up, and you realize that that's what you like about long road trips alone.

A week or so ago, I got my annual review letter from my graduate program. I think I've had a pretty good year, so it's good to see that the faculty agree! Here it is:

We are glad to sce amd hear about progress un your rcsearcll and to focus on research as much are posasìble. You also need to form your reßearclr colllrllittcc sometilile during the next year and move tow'ards ther-sí:-: proposal (noto that the approval of research ooinniittoe requires University Grziduate School involvement and rnay take Lime). We are glad to see that your work with Prof. Newton is going well.

In summary, your progress is satisfactory and your support as an Associate Instnlctor will continue (if liocessary). We are looking forwzml to _voor nlonts in the coming year.

Oh, no, wait. That's the Google Docs OCR of the scanned PDF I received. Here's what it actually said. *clears throat*

We are glad to see and hear about progress on your research and encourage you to focus on research as much as possible. You also need to form your research committee sometime during the next year and move towards thesis proposal (note that the approval of research committee requires University Graduate School involvement and may take time). We are glad to see that your work with Prof. Newton is going well.

In summary, your progress is satisfactory and your support as an Associate Instructor will continue (if necessary). We are looking forward to your achievements in the coming year.

Since the last letter in spring 2011, I: gave my second invited talk (as part of the Alumni Scholars Program at Grinnell); served as a paper reviewer for the first time (for PLPV 2012); officially finished coursework; applied and was accepted to Ph.D. candidacy; completed my first internship at Mozilla and was invited to return for a second one; and started working on research with my new advisor, Ryan. So, I'm not doing too badly, but although the letter doesn't say so explicitly, it's past time for me to start publishing my work. The way to "move towards thesis proposal" is to publish at least one paper about the work that Ryan and I have been doing. I'm workin' on that. Once we have a paper, I think that a proposal will be a natural next step.

On March 31st, I celebrated my 30th birthday by running the IU Mini Marathon for the first time!

I'd heard about the notoriously hilly IU Mini course, but this year I finally experienced it for myself. As we were lining up at the start, I mentioned to an acquaintance from Alex's and my running group that it was my first time on the course. She pointedly said, "This is a Ben Bartley course." Ben is the training director for our group, and he's also a member of the IU Mini steering committee; I'm not sure if he was personally responsible for mapping the course or not, but whoever did it seems to share his affinity for hills. It was great! It took me through some parts of town that I hadn't really seen before, as well as parts that I know and am fond of, and I think it did a decent job of showing off Bloomington to out-of-town folks who came in for the race -- like Chris chrisamaphone, who had an excellent race and finished rather faster than I did. Alex oniugnip also had an excellent race, finishing in 1:33:24 (and winning a pair of Vibram FiveFingers for being the first runner to cross the finish line wearing them). Here's a great picture of him airborne somewhere around mile 2.

I was hoping to beat my 2:06:31 half marathon PR from a couple years ago, and I thought I might even have a shot at finishing in under 2 hours, but I came in at 2:10:01, which was 34th of 56 runners in my division. Aside from the hilly course, my other (and less defensible) excuse for my slow time is that I honestly didn't know when to start running! Alex and Chris had apparently investigated the timing situation beforehand and known what was up, but I had just assumed that the race would work like every other road race I've been in since 2004, where you get an RFID device to wear and there are mats at the start and finish that record the time when you run over them. Your time for the race is the difference between the two. It's a great system, because it eliminates the need to jostle for a position close to the starting line. Instead, people sort of just mill around in the general vicinity of the starting line until the race begins, and then they start at their leisure.

At the Mini, we also had RFID whatsits, so I wasn't expecting anything out of the ordinary. My acquaintance from the running group and I were idly chatting when suddenly a starting gun went off somewhere up ahead of us. "Oh! Uh, is that the start?" "Um, maybe?" We shrugged, then made an awkward, shuffling start, not sure if we were actually supposed to be running yet or not. I couldn't see what was ahead of us on the road, because it was filled with other shuffling would-be runners, but I supposed that somewhere up ahead, there was going to be a mat to run across. But when we'd all been shuffling along for some time and no mat had been in evidence, I figured that, well, the race must be on. As it turned out, everyone's clock had started simultaneously when the gun went off, and instead of a mat at the finish line, they had funky overhead antennas -- you can see what those looked like in the top right corner of this picture of me finishing. So I probably lost thirty seconds or so to that. I'll know better next time.

The race was part of my current round of marathon training -- Alex and I are both running the Toronto Marathon on May 6. In fact, the half marathon happened to fall on a weekend when I was supposed to do the first of two 20-mile training runs for the marathon. Obviously, that wasn't going to happen, but since the program I'm using called for a 20, a 12-mile recovery week, and then another 20, I figured I'd just do the two 20-mile runs on back-to-back weekends after the half marathon. That would have sort of been asking for trouble already, but what I actually ended up doing was even worse -- I procrastinated on the first 20, then crammed both of them into last week, only five days apart. It was the first time I've ever done two runs that long that close together, and I can't say I really recommend it. I seem to be fine now, though.

Now that the toughest part of training is over with, I'm really looking forward to Toronto. The course actually has a negative drop in elevation, which I think bodes well for a PR. I'll try to go out somewhere between the 4:15 and 4:30 pace groups and see where that gets me. By the way, in case you're wondering what the most 1337 way to run a sub-4:30 marathon is, I'm pretty sure it's 8 5km blocks in 32 minutes each, then the last 2.195km in 13:37. Total time: 4:29:37. Sadly, this is 21 seconds slower than my PR. Otherwise, it would totally be my goal for Toronto.

Last week, I went to Boston for a few days to work with Amal on our ongoing multi-language parametricity project. We got some solid work done before hitting a roadblock on Friday afternoon and realizing that we're going to have to go back and rework a number of things in order to show the second result that we want to have in our paper. Our first result -- that one can combine a static language that has parametric polymorphism with a dynamic language, and still have guaranteed parametricity in the combined language by way of a run-time "sealing" technique -- is feeling solid now, but the second result still needs a lot of work. It tries to leverage the first result to prove that parametricity is also guaranteed for contracted terms in a purely dynamic language (where the contracts are implemented by embedding dynamic terms in the static language at types that are the static counterparts to whatever contracts you want 'em to have, and then immediately embedding those terms right back in the dynamic language). You wouldn't think that proving this second result would be too much of a leap once the first result is in place, but there are some really nasty bits when you actually try to do it.

I did have a cute contracts-are-not-types realization on Thursday afternoon. In a dynamic language, there are no type variables, no type abstractions, and no type applications. So that means that when we define the relatedness of two untyped terms that have a ∀α.τ contract on them -- meaning that at runtime, they are supposed to behave like parametrically polymorphic functions -- we can't define it in terms of the relatedness of their subterms. In fact we can't even talk about their subterms, because we don't know anything about the structure of the terms to start with -- they can't be type abstractions, because those don't exist! Instead, we have to say that two terms that are related to each other at the ∀α.τ contract are also related to each other at the τ contract, in an extended contract environment that has a binding for any free αs in τ. At first, I was all, "Wait, what? Which type are they actually?", and then I realized that that was the wrong question.

Anyway, today I scanned and sent Amal the seventeen handwritten pages that I produced over the three days I was in Boston; they'll be a starting point for sorting out the remaining nasty bits. I'm not gonna lie: this project has been long and difficult, and I'm looking forward it to being done this year. (It will be done this year!) But I've gotten a lot out of it; Amal pointed out that if I go to OPLSS this summer, there won't be anything new to me in the material she's presenting. That was good to hear -- both because it makes me feel like I've truly learned something, and because a little break, in between trying to absorb new material from all the other OPLSS speakers, will be most welcome if I do go.

Today, I reached the halfway point in my current round of marathon training! Something I've learned over several years of marathoning is that I can pretty much do what I want during the rest of the week, as long as I faithfully do the long runs every weekend. This time, I'm doing the long runs from the venerable Hal Higdon "Intermediate 1" training program. I haven't been following the program during the rest of the week at all; I just run when I want to, and that ends up being only once or twice a week aside from the long runs. So I'm running rather low weekly mileage for someone who purports to be training for a marathon, but it seems to be working out okay. I've managed to keep paring down my marathon PR over the years, and I've never had an injury.

When I train, I can't go as fast as I can go when I'm in a race. This is true for a lot of runners, but I'm always amazed at the huge effect it has on me. For example, here's a post I wrote in 2008, a week before my fourth marathon. I had just done my last long training run before the race, and I'd had to push myself hard to run 12.6 miles in 2 hours and 20 minutes. I reasoned that even if I were able to keep up that difficult pace for the whole marathon, it would have meant a time of 4 hours and 51 minutes. Therefore, I surely had no hope of beating my previous PR of 4:40:40. At the time, I figured that some slowdown was inevitable, because I weighed 20 pounds more than I had when I'd run the 4:40:40. But in the actual race a week later, I PRed with 4:39:46, additional 20 pounds and all.¹ Since then, I've had a lot of respect for the mysterious power that race day holds. The energy coming from the crowd, the anxiousness to perform well, the fact that people are handing you cups of Gatorade -- these things really help!

Since I know that my body is capable of my race pace, if I somehow could get myself to train at something like that pace, maybe that would mean that in the next race, I could go significantly faster. With that thought nagging at me, I've been trying to work on upping my training pace this year. Today the schedule called for running a half marathon, and Alex oniugnip came along to help pace me. We don't do all that much running together; he's a lot faster than I am, so it's no fun for anyone. But I thought that with his help, I might run at something more like race pace. And today, it worked pretty well! We ran 13.47 miles (we were defining "half marathon" loosely) in 2:14:26. I'm not going to make any promises at this point, but if I could keep that pace up for a whole marathon, I'd be running 4:21:40, which would be a new PR and one I'd be very happy with.

In other news, I continue to use Fitocracy to track my workouts, and I've got a funny story about that. On Fitocracy, you "unlock achievements" upon reaching various fitness milestones, and a lot of the achievements have cute names. For instance, the one for logging 20 miles in your lifetime (which is the only running-related one I've gotten so far, although I'm on track for the 200-mile "Hallowed Harrier" achievement by probably April or so) is "I Seem to be Lost". A few weeks ago, I noticed that the biggest and best running-related achievement, for logging 1000 miles, is called "The Shadow of Iris" -- or, at least, that's what I thought it was called. I wondered what the name meant, so I googled a bit and eventually concluded that it must be a literary reference, a line from near the end of D.H. Lawrence's The Rainbow. I was impressed! I wasn't sure what it had to do with running, but it was more than I expected from, you know, three snot-nosed startup kids.

But then, after looking at more Fitocracy profiles and seeing what achievements various people had available to them, I realized that the name of the achievement differs for male and female profiles.² It's "The Shadow of Hermes" for men. Hermes, of course, is one of the Twelve Olympians you probably learned about in middle school; he's the god of athletes and has winged sandals. Iris, it turns out, is another Greek god; she "travels with the speed of wind from one end of the world to the other" and shares "messenger of the gods" duties with Hermes. Okay, cool, but how silly that the name of the achievement has to be gendered. Why can't everyone seek the shadow of Iris? Or the shadow of iris, for that matter? I kind of enjoyed believing that the Fitocracy founders were more well-read than I am.

Back in September, I wrote about what the first half of grad school was like for me. That post covers a period of about three years, from the middle of 2008 to the middle of 2011. I've been wanting very much to write the companion piece covering the second half of grad school, but so far, I've been hampered by the fact that most of the second half of grad school has not actually transpired yet.

( Still, I'm willing to give it a shot! )

I got lots of responses to my challenge problem last week. Thanks for playing! I was going to call this post "Nerdsnipe challenge!: postmortem", but as it turns out, this won't be the end of it.

( I claimed that the problem came up in real life, but that depends on what you want to count as "real". )

Whenever I post one of these challenges, it's exciting to see the diversity of approaches that people take in responding to them. The comments are always fun to read (despite, or perhaps because, their inevitable degeneration into dick jokes). But as much as I might have nerdsniped some of you with this, the person I nerdsniped the hardest was myself. I've been thinking about this strange little problem nonstop for a week. Incidentally, we decided that the paired puzzle cards, whether pre-paired or not, would be too much work and too error-prone, and we came up with an entirely different way to get players into teams of appropriate sizes. So I'm not actually giving away anything about the game by posting all of this, plus, we're no longer plodding through the dismal realm of Applicable to a Real Situation and, instead, are frolicking through the grassy meadow of Just For The Hell Of It. Hooray!

Each player in a game is dealt two cards: one question card chosen from a set of 8 questions, and one answer card chosen from a set of 8 answers. There are 17 copies of each card, so there are a total of 8 * 17 * 2 = 272 cards. Conveniently, there are 136 players, so there are exactly enough cards for everyone to get one question card and one answer card.

The question and answer cards correspond to each other (question A goes with answer A, question B with answer B, and so on), but the dealer makes sure that nobody gets a question and answer card that go with each other. That is, if I happen to have the card for question A, I won't also have the card for answer A. Instead, I'll have one of answer cards B through H. (We can assume that the cards are dealt randomly, except for the caveat that nobody ever gets a corresponding pair of question and answer.)

Once cards are dealt, players have to find and form groups with all the other players for whom one of the following is true:

1. the other player has the same question and same answer.
2. the other player has the corresponding question and corresponding answer.

For example, if I have question A and answer D, I should group up with any players I find who also have question A and answer D, and with any players I find who have answer A and question D. (But I don't group up with players who have, say, question A and answer B, or, say, answer A and question H.)

Players can talk to each other, show their cards freely, and so on. (Let's assume that players don't lie about their cards or withhold information from each other.)

What I want to know is: how big are the groups that players form? And if not all the groups are the same size, how big are the smallest and largest groups?

This is actually a problem that arose in real life! But I won't tell how it came up until I start seeing your solutions. Go! Estimates are fine; precise solutions are also welcomed. (And feel free to ask clarifying questions; it's possible that I left out something.)

I think we've decided that we're doing Toronto in May. Training season is on!

I missed a planned run last Thursday, because it was snowing and windy (and because Chris chrisamaphone was visiting, and some things are more important than working out), but I redeemed myself yesterday by running a bit over nine miles, my first really long run of the season and probably the longest run I've done since the race last March. It's nice to know, now, that there's a sidewalk or otherwise paved surface along every inch of that route; I wasn't sure of that when I started out on it. Also, the B-Line Trail has been under construction since around the time I came to Bloomington, and although I've been running on it for a while, it's only been recently that a few big chunks have been completed. This was the first time I'd run the whole length of the finished trail. It was great!

Prompted by Alex oniugnip and by Chris, at the beginning of the year I started using Fitocracy to record my workouts. (It's invite-only; let me know if you'd like one.) So far, I have mixed feelings about Fitocracy. For a while, I was all hmph-social-networks-goddamn-kids-these-days and hmph-I-don't-need-your-carrot-dangling-gamification-nonsense-to-make-me-work-out-I-like-working-out-for-its-own-sake-dammit, but at this point I'll freely admit that the carrot-dangling gamification nonsense actually fucking works and is is fun. Kudos to them. On the downside, I've stubbed my toe on the UI a bunch of times, and I'm annoyed that there's no good way to get all my painstakingly recorded data out -- not that I can think of any particular reason why I'd need it.

For my 200-character-limit Fitocracy profile, I wrote, "Working on my seventh marathon and on my first Ph.D." Seventh! That's insane.