Skip navigation
Please use this identifier to cite or link to this item:
Title: Verified Optimizations for Functional Languages
Authors: Paraskevopoulou, Zoe
Advisors: Appel, Andrew W
Contributors: Computer Science Department
Keywords: compiler correctness
compositional compiler correctness
functional programming languagegs
logical relations
Subjects: Computer science
Issue Date: 2020
Publisher: Princeton, NJ : Princeton University
Abstract: Coq is one of the most widely adopted proof development systems. Itallows programmers to write purely functional programs and verify them against specifications with machine-checked proofs. After verification, one can use Coq's extraction plugin to obtain a program (in OCaml, Haskell, or Scheme) that can be compiled and executed. However, bugs in either the extraction function or the compiler of the extraction language can render source-level verification useless. A verified compiler is a compiler whose output provably preserves thesemantics of the source language. CertiCoq is a verified compiler, currently under development, for Coq's specification language, Gallina. CertiCoq targets Clight, a subset of the C language, that can be compiled with the CompCert verified compiler to obtain a certified executable, bridging the gap between the formally verified source program and the compiled target program. In this thesis, I present the implementation and verification ofCertiCoq's optimizing middle-end pipeline. CertiCoq's middle end consists of seven different transformations and is responsible for efficiently compiling an untyped purely functional intermediate language to a subset of the same language, which can be readily compiled to a first-order, low-level intermediate language. CertiCoq's middle-end pipeline performs crucial optimizations for functional languages including closure conversion, uncurrying, shrink-reduction and inlining. It advances the state of the art of verified optimizing compilers for functional languages by implementing more efficient closure-allocation strategies. For proving CertiCoq correct, I develop a framework based on thetechnique of logical relations, making novel technical contributions. I extend logical relations with notions of relational preconditions and postconditions that facilitate reasoning about the resource consumption of programs simultaneously with functional correctness. I demonstrate how this enables reasoning about preservation of non-terminating behaviors, which is not supported by traditional logical relations. Moreover, I develop a novel, lightweight technique that allows logical-relation proofs to be composed in order to obtain a top-level compositional compiler correctness theorem. This technique is used to obtain a separate compilation theorem that guarantees that programs compiled separately through CertiCoq using different sets of optimizations can be safely linked at the target level. Lastly, I use the framework to prove that CertiCoq's closure conversion is not only functionally correct but also safe for time and space, meaning that it is guaranteed to preserve the asymptotic time and space complexity of the source program.
Alternate format: The Mudd Manuscript Library retains one bound copy of each dissertation. Search for these copies in the library's main catalog:
Type of Material: Academic dissertations (Ph.D.)
Language: en
Appears in Collections:Computer Science

Files in This Item:
File Description SizeFormat 
Paraskevopoulou_princeton_0181D_13547.pdf986.82 kBAdobe PDFView/Download

Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.