Greg Morrisett: Scalable Formal Machine Models. CPP 2012: 1-3