Committee

  • Andrew Appel (advisor)
  • David Walker
  • Zak Kincaid

Title

Formal verification of closure conversion

Abstract

CertiCoq is a formally verified compiler for dependently typed functional languages that aims to bridge the gap between certified high-level programs and their translation to a low-level machine language. In this talk I will describe the process of implementing and proving correct, using machine checked proofs, the closure conversion phase of CertiCoq. The main transformation is preceded by a lambda lifting phase, that can be seen as an unboxing optimization for closure environments, and followed by a hoisting transformation, which flattens the structure of function definitions. As opposed to previous closure conversion implementations, our implementation decouples the lambda lifting phase from the closure conversion phase, allowing us to achieve a more modular design which is more amenable to formal verification. I will explain the implementation of the three phases as well as the proof techniques that were used to prove their correctness. Finally, I will focus on the challenges involved in the composition of the correctness proofs of the three phases.

Reading List

Papers

  • Closure conversion
    • Zhong Shao and Andrew Appel, "Efficient and safe-for-space closure conversion"
    • Amal Ahmed and Matthias Blume, "Typed Closure Conversion Preserves Observational Equivalence"
    • Yasuhiko Minamide et al., "Typed Closure Conversion"
  • Compiler correctness
    • Nick Benton and Chung-Kil Hur, "Biorthogonality, Step-Indexing and Compiler Correctness"
    • Yong Kiam Tan et al., "A New Verified Compiler Backend for CakeML"
    • Georg Neis et al., "Pilsner: A Compositionally Verified Compiler for a Higher-Order Imperative Language"
  • Extending Coq with effects
    • Aleksandar Nanevski et al., "Ynot : Reasoning with the Awkward Squad"
  • Parametricity and Relational Reasoning
    • John Reynolds, "Types, Abstraction and Parametric Polymorphism"
    • Philip Wadler, "Theorems for free!"
    • Andrew Appel and David McAllester, "An Indexed Model of Recursive Types for Foundational Proof-Carrying Code"

Textbooks

  1. Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002.
  2. Glynn Winskel. The Formal Semantics of Programming Languages.