Unless each variable can only be used once, isn't it possible to overwrite a declaration x:tau by x:sigma in a different context? This seems to make concatenation nonsymmetric (and one loses the projections as well). Computer Scientists here tell me that the ability to overwrite type declarations is essential for their work. I haven't read the paper in question but I can comment on this. In most presentations of typed \lambda calculi (e.g. Barendregt's PTS) this case (repeated use of the same variable) is excluded. Indeed it does not matter for the expressibility of the system because we can always consistently rename variables (\alpha conversion). Actually I prefer to use deBruijn indizes anyway. The translation of named variables into those indizes is certainly a matter for people writing compilers (i.e. handling a symbol table) but it should not be confused with the \lambda calculus. This two issues can and should be treated completeley seperately. DeBruijn indizes precisely correspond to projections and the usual operations of substitution and weakening have nice categorical explanations. Named variables are a complete redherring. Thorsten Altenkirch And there's a hand, my trusty fiere, Laboratory for Foundations And gie's a hand o' thine, of Computer Science And we'll tak a right guid-willie waught University of Edinburgh For auld lang syne! ==============================================================================