Lambda the Ultimate

World’s first formal machine-checked proof of a general-purpose operating system kernel from Planet Haskell.

Some previous work has been mentioned here before, but I don't think there has been a story on any of the previous work.

Many loops in probabilistic inference map almost every individual in their domain to the same result. Running such loops symbolically takes time sublinear in the domain size. Using normalization by evaluation with first-class delimited continuations, we lift inference procedures to reap this speed-up without interpretive overhead. To express nested loops, we use multiple control delimiters for metacircular interpretation. To express loops over a powerset domain, we convert nested loops over a subset to unnested loops.

The paper is a bit hard to follow, but there are enough little tricks here to merit attentive reading. Or better yet, read the code. The basic PLT idea might be summed as doing abstract interpretation on a shallowly embedded DSL using delimited continuations.

I'm pleased to announce the Eastwest programming language and structure editor. This is a research project aimed at exploring how structure editors can help with functional programming. Eastwest introduces the concept of "token type", which is a useful way of handling bindings in structure editors. For beginners, the most interesting feature of Eastwest is that the type of an expression is always displayed at the top of the screen. Eastwest takes into account the type of an expression when displaying suggestions. Arguments can be placed anywhere inside function names which can be written in any character set thus opening the possibility of making source code resemble human language. The structure editor can handle thousands of nodes. Since it is impossible to copy/paste source code, I've created a series of videos showing how to use the structure editor and the language.

the project can be found at
http://sites.google.com/site/rathereasy/eastwest
the video tutorials can be found at
http://sites.google.com/site/rathereasy/eastwest/tutorial
You can download and try it out at
http://sites.google.com/site/rathereasy/eastwest/get-it-

Eastwest is based on the O'caml Structure Editor Toolkit (OSET), which can be found at
http://sites.google.com/site/rathereasy/oset

If anyone knows of any similar projects, please let me know.

We all know that, in many languages, null is very semantically overloaded. Has anyone attempted to separate and enumerate its various meanings? A few spring immediately to mind:

• Empty list, set, dict., etc. (one or many?)
• No object
• No value
• Uninitialized

What others are there?

(I am a long-time, on-and-off lurker, first-time poster. Etiquette corrections are welcome.)