Our research group is working on the design and implementation of new forms of procedure calling protocols based on the notion of linear naming, together with relevant supporting formal tools and implementation technology.
Computer science is largely the study of naming. The addresses in memory systems, the variables in programs, the pathnames in filesystems, and the URLs printed in magazine ads are all names. Giving something a name gives us power over it, enabling us to save it for later or tell someone else about it. The ability to name something is the ability to share it.
But the power to name and share things does not come for free. There is always a small amount of overhead, roughly proportional to the number of outstanding copies of the name, required to support sharing.
These observations have lead us to investigate linear naming. A linear name cannot be duplicated, so it requires only a small fixed amount of overhead to implement. The logic of linear naming is linear logic, which provides a different (and logic-independent) algorithmic way of thinking about procedure calling, naming, closures and thunks, and explicit control. Linear logic is a ``resource conscious'' logic that is ideal for studying issues of resource management and explicit control of evaluation.
Our study of linear naming has yielded many interesting theoretical insights, and we believe that it is now ripe to yield pragmatic new implementation technology - especially for distributed computation, where the costs of sharing can be particularly pernicious.
Our research group is associated with the Church Project.
We've got some code and we've written some papers. There should be more pointers here, but a good way to get started learning about what we do would be to read this working paper that describes our goals.