There is a new paper on gradual typing available on-line at http://cimini.info/publications/criteriaForGT.pdf by Siek, Vitousek, Cimini and Boyland (I suspect it is a submission to SNAPL). While I haven't had a chance to read it in detail, it talks about the "gradual guarantee" of such systems and includes a short section on Boyland's analysis of Grace. Kim