Tagged variables in typed lambda-calculus - references?

Hi,

I'm trying to find references to versions of the typed (but also

untyped) lambda-calculus. The kind of thing I'm looking for is

*

%x . E

where % is a lambda-sign, x is the bound variable, * is a tag and E is

a lambda-term with occurrences of x in it. The tags can have any

meaning, although I'm looking to give them an opeartional

interpretation about the reduction behaviour of the term.

Has there been any previous work on this? Does anyone know of any

other bboards, lists where I can enquire?

Thank you

Simon

-------------------------------------------------------------------------

Dept of Computer Science, University College London, London WC1E, England