What's your topic? I don't know how quals at Indiana work.

Joe Stoy's textbook on denotational semantics looks wonderful, but I've only read a little. There's also Tennent's _Semantics of Programming Languages_, and while it's not standard at all (and I'm also biased), I think the chapter in _Design Concepts in Programming Languages_ (http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11656) on denotational semantics would be great for building intuition.

The quals process has changed since I got here, and I'm one of the last few people to be using the old process, which entails taking two written exams ("theory" and "systems") and then taking an oral exam in one's particular research area. Some of the guidelines given for the oral are:

• "The oral qualifier examines your deep knowledge of a research area (e.g., databases). Within that specialized area, coverage should be broad; the area should not be construed as the thesis topic."
• "The oral is not for presentation or examination of your research plans, which are examined in the proposal defense."
• "Unlike the written qualifiers, which test breadth, the oral area qualifier tests your knowledge and mastery of the more specialized research domain in which you expect to do your research."

So, to answer your question, my topic is "programming languages", but since that's hopelessly broad, my topic is actually more like "semantics of programming languages and type systems". There's a slant toward systems that admit flexibility in the amount of static verification of types, because that's what I'm finding I care about, but I can't just do that, since I think it would be considered too narrow a topic for the oral.

(The new quals process seems better in terms of actually assessing one's ability to do research, but I was already partway through the old process when they made the switch, so I decided to just keep going with it, for better or worse.)

...I forgot about Turbak and Gifford! I should look at that denotational semantics chapter. When the book came out last year, Dan told me that he might just stop writing textbooks. Of course, Dan can be a little dramatic sometimes.

I second the Turbak and Gifford for denotational semantics. Olin taught from a draft version of that for a semantics course back in '03 or '04, and I thought it was a good place from which to learn such things.

I just borrowed it from Dan. I actually had to drive to his house to pick it up this evening because he deemed it too heavy to drag to campus. (It is a huge brick of a book. Amazon says it's both larger and heavier than CLRS.)

"semantics of programming languages and type systems" is still pretty broad indeed, or perhaps I've just been in academia too long :-)

Yeah, it is. But I think that that's the kind of breadth that they're looking for with the oral qual.

So disclaimer the closest I ever came to taking a qual was when Aquinas, one of Andrew Appel's students, taught me TAPL as part of his quals preparation. So I don't actually know how this works.

Chris, do you recall how this unification paper went? For some reason I'm having trouble paging it back in and I'm off campus. Unification is also covered in the "Type Inference in Context" paper by McBride etc which I understood much better after I rewrote it twice.

Also, what are you looking to get out of the Substructural Type Systems paper? (First thought) In my recollection it's alright at explaining substructural type systems, but not really at giving a feel for substructural logic. (After browsing the Google Books non-redacted part) Actually, I think my thought is more that, there are so many paths through this subject, and I don't know if the particular path Dave Walker chose is the one I find most interesting. Another alternative would be Dave Walker and Limin Jia's joint papers (ILC: A Foundation for Automated Reasoning About Pointer Programs, in my case, is bright glowing red on my papers-to-read queue).

Ooh, that's a good idea -- I need someone to teach TaPL to! Who can I get?

So at CMU do you not have quals as such?

What I'm looking to get out of the Substructural Type Systems chapter is to be able to hold up my end of a conversation with Amal about linear and affine types and suchlike.

At CMU we do not have quals as such. I guess the ATAPL chapter is right on target if what you're actually interested in is substructural type systems, so whoo :).

I love how you guys do things. The upsetting thing that I notice about the quals process, now that I'm getting close to the end of it -- and I'm not talking about IU specifically here, but about quals as they are at a lot of schools -- is that quals are kind of like "Okay, now that you've been in grad school for years, now you have official permission to conduct real research in your field." Before that, you were presumably only supposed to be doing "exploratory" research, or something. At CMU it appears to be more like "If you are not doing real research from day one, what the hell is wrong with you? Stop taking classes."

I think this is true. On the other hand, in my retrospect I think I could have used an excuse, maybe around year 2, when I was told "okay, research is not your primary job for just a month or two. figure out what you still need to know. learn it." You won't have an excuse after this point in time.

Because as it is, a lot of us have a bumbly moment where we realize oh shit I need to know this and I don't and here's me getting called out on the floor. And then I think the idea is you figure it out. Quals, in that respect, are actually a bit of a nice safety net, but that is an aspect of quals that is disconnected from the idea that what you're doing is qualifying.

*applauds*

The Sheard paper, while extremely cool, probably isn't the right one for my oral quals list -- but maybe the Cardelli is! That's another one we looked at for the FLOPS submission. (Actually we cited Sheard, too, for path compression, because you told me about it.)

The Goguen "What Is Unification?" paper was one of the ones I read when I was working on the triangular substitution stuff. I didn't have the category theory to understand a lot of it, but I liked it.

(Goguen worked on so many interesting things. In my pre-grad-school explorations, before I was consciously aware of being interested in most of the things I'm interested in now, I kept arriving back at his website. In fall of 2006, I remember being very excited about applying to UCSD to work with him and then suddenly finding out that he'd passed away. That was a dark few days for me.)

I'm assuming you don't need to know anything about...

Yeah, for this I don't. I'm not even entirely sure if I want to include the stuff about unification at all, because it doesn't have much to do with what I'm doing now -- but if part of the point of orals is to sum up what I've been doing for the last two years, then it makes sense to include it. And I would like to get back to it at some point. You know, in my copious free time.

But...but the whole point of indexed possible-worlds models is premised on the idea that domain theory is scary and to be avoided!

In all seriousness, I don't want to get too heavily into denotational semantics and its domainy underbelly, at least not right now. I just need to do enough of it so that I have a clear understanding of what I'm not doing most of the time.

> TaPL, like, all of it

Oh man, I cannot recommend this book highly enough. When it was finally shoved into my hands in year, I think, three? Of my degree, so many lightbulbs went on.

I think about a quarter of my thesis was just paraphrased bits from TaPL. (Cue old joke about the difference between "plagiarism" and "research"...)

I honestly don't know what people in my field did before TaPL.