## Define double spacing

I just spent far too long with someone at the graduate office trying to get a concrete understanding of how they define double spacing. I tried my best to explain that I cannot just put an extra »line« between each line of my document.

All information I have been able to obtain elsewhere seems to indicate that what they really want, but do not seem to know it, is one and a one-half line spacing. That is in LaTeX you would set \baselinestretch to 1.5. I am almost certain that this is what I should be doing, but the woman seemed to think that I wanted there to be twice as much space between baselines.

I tried to take the approach of getting concrete and asking that if I used a 10pt font, what should the measurement be between the bottom of one line and the next. However, to my surprise the woman I spoke with claimed that they do not actually measure this, they just look at it and »know«.

So we agreed that I would just fax her a sample and she would let me know whether it looked correct.

Surprisingly, the definition of double spacing is something that the Chicago Manual of Style does not address.

## Defense against the dark arts

This Thursday at 9AM  I will defend my thesis against my committee, and anyone else that shows up and attempts to ask me difficult questions. But really, who would want to get up that early to do that?

Assuming that I can successfully disarm two assistant and two full professors,  I will be all set to start working on Scala related things at EPFL.  Of course, I've bought a plane ticket to Geneva, Switzerland for the 26th, so unless my rhetorical-fu is truly mediocre, that will be happening one way or another.

## Getting closer to completion

I finally fixed most of the issues that were preventing me from building my dissertation using Gentzen. Here is an inference rule out of my dissertation, using Gentzen:

And here is the same rule using the Euler package:

Unfortunately, the column width of this theme does not allow making the images much wider. It is fairly difficult to get a good idea of the differences by looking at them. So I've also provide page 29 of my dissertation in both versions: Gentzen and Euler. It is also a good way to emphasize that, on a printed page, many of the details I've agonized over are pretty subtle if you are not looking for them. Some of the spacing is off in places in the Gentzen version, but I need to investigate further whether that is because of the font itself or my macros for it.

However, I've also provide an update version of my table of symbols:

Notably, I've finished \leadsto, \in, \bullet, and \cdot. I've included \star from one of the LaTeX symbol fonts I believe.

In any event, I am certainly interested in feedback — assuming there are opinions on how it is looking.

## Curation woes

I would like to know if M. O. van Leer has a first name and perhaps even exists. As far as I can tell he was a co-author on a FPCA paper on Clean in 1987, has not published anything since, and is not listed as a former member of the Software Technology Research Group in Nijmegen.

## Step one complete, and an upgrade

I've finally handed off a draft of my dissertation to my committee. I hope that I will find time to update more frequently from here on out.

In other news, I've finally taken this opportunity to upgrade to the latest version of WordPress in the hopes that it will prevent the spread of that malignant blogroll spam that you may have been noticing. I guess this is what happens when you run software written in PHP. Maybe I will have time to think about a custom theme before too long as well.

## Jean-Yves Girard’s evolving opinion on disjunction

1995: "Only a masochist would state AB  when he knows A."

2003: "Only a moron would state AB  if he has obtained A."

While I have been in hiding, toiling on my dissertation, a rather large number of links have been accumulating in my to-do list. I'll hopefully write more on the status of my dissertation soon.

Software

A few weeks ago I became frustrated with the capabilities of FontBook on Mac OS X and Gnome Specimen and gucharmap under X11. I spent some time searching and came across Linotype's FontExplorer X. My best description of it would be iTunes for fonts. Not only does it let you manage, examine, and compare the fonts you do have, it lets your preview and purchase fonts from Linotype.

I also came across the UnicodeChecker application (again MacOS X only) which perhaps provides a more detailed examination and exploration of the properties of Unicode glyphs.

Reference

I'm not sure where I read about it, but I recently came across Symbols.com, "The Online Encyclopedia of Western Signs and Ideograms". I haven't needed to consult it yet, but it is fairly interesting just to see what it gives you when asking for a random sign.

I've known about this for a while, but didn't think to mention it until now: the entirety of the Fifteenth edition of the Chicago Manual of Style can be found online. Useful when you don't want to carry around the hardcopy, and searchable. Unfortunately, looking at it again now, the fact that it says in the corner »University of Pennsylvania« makes me believe that is this probably not a free service. And indeed, I just verified this with my desktop, which does not have a cached cookie from inside the Penn network.

Theory

From Lambda the Ultimate, I learned about a paper giving a functional description of the »galleys« layout algorithm used by the lout document processing system.

This also reminded me of the earlier post, also by Neel, on a functional description of TeX's formula layout algorithm.

I also went looking and Kingston has a nice paper on the design of lout, and website on the eventual successor to lout, Nonpareil. lout is an interesting system, though for some reason when I first encountered it many years ago I didn't seem to think it produced as nice of output as TeX. I haven't tried to reevaluate this at the moment, and see whether it has changed or I was simply wrong in the first place.

Also, something else on Lambda the Ultimate led to me to discover the Juno-2 structured drawing editor. I've only had a chance to read about it briefly, but it sounds quite a bit like what I have envisioned for the font editor I've been thinking about for a while, but haven't found the time to seriously start yet.

Finally, while writing this section, I came across another Lambda the Ultimate post on Skribe, a Scheme based document formatting system. It however it seems to be more of a macro layer on top on HTML and LaTeX, rather than a fully integrated system.

## Filenames for publications

There is an unfortunate tendency for people to make papers available on their websites and give them highly descriptive names like types03.pdf or even the gem tr.pdf. I have a directory or two full of files with names like that and despite the promises of Beagle and Spotlight it is very hard to find certain documents.

I know this is something Joshua rightful complains about, and I'm admittedly guilty of this to some degree myself. So I put it on my to-do list a while back and finally decided to take a few minutes today and sort out the filenames I've assigned to my papers. However, when getting started I was faced with the dilemma of just what the naming convention should be. I did some poking around with Google, but couldn't really find any information on choices that other individuals or organizations have made.

Clearly the year and some approximation of the authors last names should be used, but there are a lot of trade-offs.

One system that I do know about is the one used by the Church Project at Boston University. If I remember correctly the filenames and pages are generated from the BibTeX entries. For example, consider the paper »Type inference, principal typings, and let-polymorphism for first-class mixin modules« by Henning Makholm and J. B. Wells. This paper gets a web page named http://types.bu.edu/reports/Mak+Wel:ICFP-2005.html and a PDF file with a very long name. So long that I will instead just describe the format: the last name of the authors separated by the plus symbol, a colon, title of the paper, a colon, conference venue, a dash, and year. While very descriptive this scheme has a few problems. Firstly, colon is a reserved character in at least a few operating systems. Secondly, is that it is just really long name. I can easily imagine one papers with several authors that the name would exceed the common 255 character filename limit that many filesystems have.

So if anyone has suggestions for developing a consistent naming convention, let me know. While more descriptive filenames would be useful, perhaps what is really needed is the metadata equivalent of »ls«. Then we would be in the position to simply complain about the fact that people don't fill in the metadata fields of their documents.

## Research versus engineering

You know you're doing research when you spend today undoing nearly everything you did yesterday.

## Document first, implement later

Lately, in terms of »research« I've been working on a draft of the InforML manual. It is one-half specification, one half tutorial. The general idea being that if I have thought through everything well enough to explain how to program in the language, I probably understand it well enough to know exactly what needs to be done in implementing it (or rather extending/modifying AspectML to become InforML). So far this has worked really well, as every time I sit down to rewrite the bits of my tutorial, I keep coming with things to put on my list of design questions.

Another part of the exercise has been to focus on trimming out anything in the language that isn't actually necessary to complete my dissertation. However, if the feature is already in AspectML I'll probably leave it in unless its interactions with the extensions for InforML are not well understood and/or would require sitting down and doing some involved proofs to verify.

I think I'm converging and hope to have a kind of complete tutorial and specification ready by Friday, but we'll see.