From: nicolas.oury at gmail.com (nicolas.oury at gmail.com) Date: Thu Nov 24 17:10:19 EST 2011 

It is often used to represent a function that applies on a term, or an expression. [ t ] means the function [] applied to t. In those papers, it often represent a CPS transform. Like [ x ] = \ k . k x would mean "the cps transform of 'x' is '\ k . k x' , or cps(x) = \ k . k x. Using [ _ ] is a bit nicer.
Posted on the users mailing list. 
