A Verified Implementation of Function Extraction

Functional programming languages have simpler semantics than imperative languages making verification much easier in comparison. Given this, it would be desirable to be able to take an imperative program and transform it into an equivalent functional program and then perform any analysis on the transformed program. In this thesis, we will both describe a method to transform an imperative program into a functional program as well as implement this method in Gallina/Coq. We then prove the correctness of this method by way of Hoare Logic. Specifically, we will demonstrate that the equivalent functional program forms a valid Hoare triple for the original imperative program. Thus, we will be able to reason about the functional program and apply the results to the imperative program.