Advisor meeting went okay. kw popped in and started a discussion of aleksey's stuff: verifying a garbage collector at a very low-level. Involved omewhat confusing but intriguing consequences of linear (meta-)theorem representation and checking.