George C. Necula: Using Dependent Types to Port Type Systems to Low-Level Languages. CC 2006: 1