Lambda the Ultimate

Environment Classifiers
started 2/19/2004; 2:56:13 AM - last post 2/20/2004; 2:30:05 AM

Ehud Lamm - Environment Classifiers

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

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

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.