The first place I encountered this notation is Joseph E. Stoy Denotational Semanatics: The Scott-Strachey Approach to Programming Langauge theory The MIT Press, 1977 I quote from page 29: The brackets [[ ]], used round an argument of a semantic function, always enclose expressions in the object langauge, possibly including metalanguage variables. There appears to be no discussion of the history, other than Stoy perfers this to Quine's quasi-quotes (Quine's corners) Unfortunately, this book is, I believe, out-of-print. Regards to all, David ==============================================================================