Lambda the Ultimate

A Formulae-as-Types Interpretation of Subtractive Logic

We present a formulae-as-types interpretation of Subtractive Logic (i.e. bi-intuitionistic logic). This presentation is two-fold: we first define a very natural restriction of the lambda-μ-calculus which is closed under
reduction and whose type system is a constructive restriction of the Classical Natural Deduction. Then we extend this deduction system conservatively to Subtractive Logic. From a computational standpoint,
the resulting calculus provides a type system for first-class coroutines (a restricted form of first-class continuations).

Yet another connection between subtractive logic and control. I remember the author mentioned on LtU, but I cannot find any citations.

I've just read one of Joel Spolsky's usual rants, this one on the joys and virtues of Hungarian notation. You can take the boy out of Microsoft …

His example is avoiding malicious user input on a web form by ensuring all unsafe input is always encoded before use. He suggests two coding conventions before settling on Hungarian Notation as the Right Thing.

Now I expect LtU readers (certainly this one) will be wondering how a flakey substitute for a type system ended up being Right Thing instead of the Real Thing we know and love (and at this point everyone should briefly murmur a prayer over their copy of TAPL). But any regular reader of Joel will know he is thoroughly pragmatic (or anti-academic, depending on your mood) and his solution fits his mindframe. So, leaving aside ranting and wailing about Joel's lack of PL education (because, frankly, I'm doing enough for everyone) let's talk instead about how one could change his mind. Specifically, implementing Hungarian is a few days of drudge-work. You're never going to get Joel to sit down with SICP, EOPL or PLAI, and TAPL, to get the necessary background to implement his own statically typed language, and if you tried he would rightly tell you it would take too long to learn. Instead, could you deliver a statically typed variant of Javascript that would catch these errors in a similar time period? If so, what tools would you use? What type systems? How practical can we make our theory?

Related to the recent "how to read papers" thread...

How do you guys organize your papers? I have a file naming scheme that's a big pain to manage and not terribly useful. I guess what I want is something like iPapers, but less tied to PubMed and cross-platform. (At least I need it to run on my Linux workstation, and hopefully on my Mac laptop...) And I guess in my dirtiest fantasies it would maybe integrate with Citeseer and CiteULike, but that's not so important to me, actually.

I'm sure semantic web types will tell me that I really want a general purpose RDF browser or something to manage general meta-data, but I'd be happy with something less general and more tailored to this domain.

Anyway, does anybody out there have a tool (or just an organizational discipline) that they're happy with? Satisfy my curiosity...