Semester's over, all finals written, all papers submitted. Finally, Freedom! I'll go back to Germany over Christmas, to morally prepare for my upcoming Thesis work.

Finally got the book commonly cited as GLT89: Girard's Proofs and Types. I've only had a look at the first two chapters so far, but this seems like a good read. Couple of other interesting things to read, too, of course; maybe I'll finally have the time to figure out what exactly inverse co-limits are, what the precise definition of cartesian-closed categories is, and why coherence spaces can describe stable functions even though they supposedly don't form this kind of category.

FreeSCI
The project at CU Boulder has officially concluded; our final paper (a very informal, light technical read) is available from the web page. In essence, it worked out quite well. People interested in the technical background behind FreeSCI's new glutton branch should definitely have a look, but I'm not sure if there are any here (still, just in case...)