Type-Based Certifying Compilation

PLDI'01 Tutorial Accompanying References


I. Introduction and Motivation


II. A Hacker's Guide to Type Theory


III. Certifying Low-Level Features


IV. Certifying High-Level Features


V. Engineering Type-Based Compilers


Copyright (c) 2001, Zhong Shao, Dept. of Computer Science, Yale University