Committee

  • Andrew Appel (advisor)
  • Aarti Gupta
  • David August

Abstract

An increasing amount of software is written and proven correct in proof assistants. For example, an optimizing compiler for C, CompCert, has been developed and fully verified in Coq, an interactive theorem prover. For interactive theorem provers to become credible programming environments, their compilation pipelines must generate production quality code. Moreover, these compilation pipelines should be proven correct, lest the guarantees achieved in the interactive theorem provers will not apply to the program being run.

Reading List

Papers

  • O. Danvy and A. Filinski. Representing control: a study of the CPS transformation. MSCS 1992.
  • A. W. Appel and T. Jim. Shrinking Lambda Expressions in Linear Time. JFP 1997.
  • O. Danvy and L. R. Nielsen. A first-order one-pass CPS transformation. TCS 2003
  • P. Letouzey. A New Extraction for Coq. TYPES 2002.
  • A. Kennedy. Compiling with continuations, continued. ICFP 2007.
  • R. Kumar et al. CakeML: A Verified Implementation of ML. POPL 2014

Textbooks

  1. A. W. Appel. Modern Compiler Implementation in ML. Cambridge University Press, 1998
  2. B. Pierce. Types and Programming Languages. 2002.
    • Part I. Untyped Systems
    • Part II. Simple Types
    • Part IV. Recursive Types
    • Part V. Polymorphism (Chapters 22-25)
  3. B. Pierce. Advanced Topics in Types and Programming Languages. ISBN 0262162288. The MIT Press, 2004.
    • Chapter 2. Dependent Types