At least in 1975 Scott, Strachey and Stoy used such [[..]] notation, but it should be possible to go beyond that, as you do yourself perhaps with the reference to Knuth and APL. The question intrigued me because my reflex was to believe that the notiation should come from good old model theory. But that seems not be the case. Fer-Jan de Vries, CWI, Amsterdam. ++++++++++++++++++++++++++++++++++++++++++++++++++++