Robert Harper
Mechanizing the Metatheory of Standard ML
