@incollection{Courant2020, abstract = {Code generation is gaining popularity as a technique to bridge the gap between high-level models and executable code. We describe the theory underlying the PVS2C code generator that translates functional programs written using the PVS specification language to standalone, efficiently executable C code. We outline a correctness argument for the code generator. The techniques used are quite generic and can be applied to transform programs written in functional languages into imperative code. We use a formal model of reference counting to capture memory management and safe destructive updates for a simple first-order functional language with arrays. We exhibit a bisimulation between the functional execution and the imperative execution. This bisimulation shows that the generated imperative program returns the same result as the functional program.}, author = {Courant, Nathanaël and Séré, Antoine and Shankar, Natarajan}, doi = {10.1007/978-3-030-39322-9_4}, journal = {Lecture Notes in Computer Science}, month = {jan}, pages = {68-89}, title = {The Correctness of a Code Generator for a Functional Language}, url = {https://zenodo.org/record/3965629/files/article.pdf}, year = {2020} }