Lambda the Ultimate

The slides for the talk discussed here are now available for download. Like all of Ken and Oleg's work, this stuff is both cool and important.

Keep in mind that the talk is quite different from the paper. The safety claims were formalized and proved in Twelf: list example, array example. To follow the proofs you should read them alongside the presentation slides. I am told that the first file might change soon, to reflect a more general proof. Perhaps Ken or Oleg would like to comment on the experience of doing mechanized proofs, a subject the comes up regularly on LtU.

LtU newcomers, who already managed to take in a little Haskell or ML, may want to spend a little time chewing on this, and ask questions if something remains unclear, since this work may eventually have practical importance, and can teach quite a few interesting techniques.

both c and c++ design doc links are outdated.

the sites have moved to http://www.open-std.org

the new links are:

c workgroup

c++ docs or better yet c++ workgroup

There has been some interest lately about Erlang on meta-sites like reddit and digg. I thought I was reading another blog entry from someone who was praising Erlang's concepts without actually writing any working Erlang systems. Then I noticed the name seemed a little familiar:

http://armstrongonsoftware.blogspot.com/

So far there's an easy going description of some of the key concepts behind Erlang. It won't be anything new for those who have read his thesis, but it is a consise high level intro to concurrency.

I'm looking forward to future entries.

[EDIT: corrected the thesis link. Thanks falcon]

In a search of Ltu there are many occurrences of the expression "dynamic semantics" usually in discussions of static and dynamic typing. It is easy enough to imagine what this might mean but I wonder if there is an accepted formal definition in computer science similar to the definitions of axiomatic, denotation, and operational semantics. I found one suggestive paper "Representing Action and Change in Logic Programs" but this doesn't directly answer the question. Does anyone know of anything? Thanks.