Lambda the Ultimate

In Cat the construction of a nullary constant generating function (e.g. a thunk) is done using the "quote" operator. It pops a value off the stack, and pushes a nullary function onto the stack. In other words the quote operation has the type: ('a -> ( -> 'a))

I could have called the operation "thunk", but I find the term discordant (a purely subjective opinion). I wonder if there are other associations with the term "quote" which suggest maybe I would be better off if I called the operation "thunk"? Perhaps there is a better term?

Any suggestions would be appreciated.

After reading many posts lauding interactive tools as an integral part of the next big thing in software development, I figured I could offer this as counterpoint. The paper Magic Ink: Information Software and the Graphical Interface very eloquently argues that most software today, especially information-intensive software (think IDEs and many other GUI-based PL tools) are really badly designed. The most memorable section subtitle being interactivity considered harmlful. This is a real treasure trove of wonderful design ideas for interfaces for information-rich applications.

This paper follows in the grand tradition of Edward Tufte, whose book The Visual Display of Quantitative Information was an incredible revelation for me.

Somehow, I do think that some of the ideas behind Intentional Software fit in here -- although I make no claim as to whether the actual implementation of those ideas is an appropriate realization.

Towards a Mechanized Metatheory of Standard ML, Daniel K. Lee, Karl Crary, and Robert Harper.

We present an internal language with equivalent expressive power to Standard ML, and discuss its formalization in LF and the machine-checked verification of its type safety in Twelf. The internal language is intended to serve as the target of elaboration in an elaborative semantics for Standard ML in the style of Harper and Stone. Therefore, it includes all the programming mechanisms necessary to implement Standard ML, including translucent modules, abstraction, polymorphism, higher kinds, references, exceptions, recursive types, and recursive functions. Our successful formalization of the proof involved a careful interplay between the precise formulations of the various mechanisms, and required the invention of new representation and proof techniques of general interest.

The way that most programming languages end up working is by defining a smaller core language to which the constructions in the base language are translated. This means that you can prove the type-safety of a programming language by showing that the internal language is type safe, and that every type-correct program in the full language translates to a type-correct expression in the internal language. In this paper, the authors carried out the mechanization of a core language for SML. The next step is mechanizing the correctness of an elaborator from SML to this core language, and then full, no-foolin' SML will have a fully machine-checked correctness proof.

I'm interested in learning more about parallel algorithms and data structures (since it looks like they're going to become more and more important), and I have access to a decent university library. Does anybody have some favorite books or papers I might read?

As usual on LtU, I'm also interested in how programming languages can make parallel programming faster, more scalable, and/or easier. So if you have some cool programming languages oriented toward parallel stuff, I'd love to hear of them so I can have a look.