Lambda the Ultimate

Recently the homepage is almost dead, and the discussions about important papers that are mentioned on the home page almost non-existent.

I am sad to say that if this continues LtU will fade away - something I am sure none of us wants.

This is a cry for help. If you are an editor, please try to post news you come across that might interest the LtU community. Take part in the discussions (you don't have to participate in all of them! participating in discussions on "static typing" is optional...) If you are an editor, are reading LtU, but haven't posted in a long time, don't feel you have become an outsider. You are still part of the team, and I for one am interested in what you might want to share. I know some long time editors got discouraged for various reasons -- I think now is a good time to return and reshape things to what they used to be.

If you are a regular reader and participate in the forum regularly, if you think you understand the spirit of LtU, how about signing up to become an editor? The process is simple (basically, you have to email me and that's it).

Many of you have personal blogs, and they are great resources. I still think the LtU community effort had an additional value it'd be a shame to lose. If you agree - post!

Finally, if you are a programming language scholar, and are reading and enjoying LtU - how about signing up to be a guest blogger?

A teaser from POPL'07: A Complete, Co-Inductive Syntactic Theory of Sequential Control and State by Støvring and Lassen.

We present a new co-inductive syntactic theory, eager normal
form bisimilarity, for the untyped call-by-value lambda calculus
extended with continuations and mutable references.

We demonstrate that the associated bisimulation proof principle
is easy to use and that it is a powerful tool for proving equivalences
between recursive imperative higher-order programs.

The theory is modular in the sense that eager normal form
bisimilarity for each of the calculi extended with continuations
and/or mutable references is a fully abstract extension of eager
normal form bisimilarity for its sub-calculi. For each calculus, we
prove that eager normal form bisimilarity is a congruence and is
sound with respect to contextual equivalence. Furthermore, for the
calculus with both continuations and mutable references, we show
that eager normal form bisimilarity is complete: it coincides with
contextual equivalence.

A draft by Takeuti Izumi

This paper defines the theories of parametricity for the system lambda-P-omega in lambda cube, and shows some of its application. These theories are defined by the axiom sets in the formal theories. These theories prove various important semantical properties in the formal systems.

Parametricity is Wadler gets his theorems for free, nad Izumi gives an example of one of these free theorems for dependent sums in the Calculus of Constructions.

Hello Lambdans:

Under the influence of tryptophan, I published a blog post giving a hobbyist's perspective on The Significance of the Meta-Circular Interpreter.

My blog's audience are mainly comprised of other hobbyists and professional programmers who dream of escape from their BigCo humdrum. As you would expect, the post lacks academic rigour and some feedback on factual errors would improve it greatly. One early version conflated self-hosting, self-interpreting, and meta-circular evaluation. Thanks to an early comment, I was able to revise the content.

What are your thoughts on the significance of languages that contain a meta-circular evaluator, a self-interpreter, or that are self-hosting? How could this post be improved (either from the perspective of accuracy or of advocacy?)

Hello Everyone,
I have posted an alpha version of a new Object System Library that I'm writing in Scheme (currently using MzScheme only). It combines the Prototypes with Multiple Dispatch object model from the Slate programming language (as described in this document) with Method Combination from CLOS (as described in section ten of this document), to create an object system which I believe to be novel (having found no evidence to the contrary). It is available from the project page or directly from the download site.

I have not had much time to work on it, so it currently only has some debug behavioral print-outs, but if anyone's interested, I could clean up the code into a portable library, and perhaps document it a bit more.

Feedback is appreciated,
Ryan Kaulakis

Note: This is an update from this earlier post.