Lambda the Ultimate

I have had many helpful comments and reviews on my recent paper about Cat, but the biggest criticism seems to be that I don't motivate the paper very well. This is perhaps the hardest thing to do!

The contribution of the paper is that it is the first time (AFAIK) that anyone has presented a type system for a pure functional stack-based language.

To understand the implications, consider if we were to introduce the ability to use primitive operations as first class values in MSIL or JVML in a type-safe manner.

So my question to the community is, is that sufficient motivation and should I emphasize these points in the paper?

I have even considered rewriting the name and abstract as follows:

Typing a Functional Stack Based Language

Stack based langauges, such as the JVML and MSIL, are very popular as VM languages, but are mostly imperative in nature; they lack the ability to treat operations as first class values.

This paper presents a formal typing discipline for a purely functional stack-based language.

Perhaps this kind of paper would be more well received by the community?

Thanks again for everyone's help!

For some reason (probably starting with the letter N), seperation logic was recently mentioned here a few times. Since this area may be relatively unknown to many readers, I thought the following two course web sites from John C. Reynolds may be of interest:

Separation Logic (Spring 2004)

Current Research on Separation Logic (Spring 2005)