Lambda the Ultimate

inactiveTopic Environment Classifiers
started 2/19/2004; 2:56:13 AM - last post 2/20/2004; 2:30:05 AM
Ehud Lamm - Environment Classifiers  blueArrow
2/19/2004; 2:56:13 AM (reads: 11241, responses: 2)
Environment Classifiers
Environment Classifiers. Walid Taha, Michael Florentin Nielsen. Extended Abstract, POPL'03

This paper proposes and develops the basic theory for a new approach to typing multi-stage languages based a notion of environment classifiers. This approach involves explicit but lightweight tracking at type-checking time of the origination environment for future-stage computations. Classification is less restrictive than the previously proposed notions of closedness, and allows for both a more expressive typing of the "run" construct and for a unifying account of typed multi-stage programming.

We mentioned code generation the other day, so I thought people here might be interested in this paper.

It is essential reading for those interested in typed staged computation.

Posted to theory by Ehud Lamm on 2/19/04; 2:57:04 AM

Frank Atanassow - Re: Environment Classifiers  blueArrow
2/19/2004; 12:01:20 PM (reads: 169, responses: 1)
This is on my reading list. Is it any good?

Ehud Lamm - Re: Environment Classifiers  blueArrow
2/20/2004; 2:30:05 AM (reads: 133, responses: 0)
The paper presents an important idea (i.e., environment classifiers), and gives detailed semantics.

This paper isn't really a fun read, though. It's worth pursuing mainly if you are interested in typing of staged code and in the connection to modal logic.

If, like me, you are interested in the modal logic aspects of this work, Pfenning and Davies's papers (refs 15 and 16 in this paper) provide a detailed introduction.