Published in

Springer Verlag, Lecture Notes in Computer Science, p. 68-89, 2020

DOI: 10.1007/978-3-030-39322-9_4



Export citation

Search in Google Scholar

The Correctness of a Code Generator for a Functional Language

Book chapter published in 2020 by Nathanaël Courant ORCID, Antoine Séré, Natarajan Shankar
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Green circle
Preprint: archiving allowed
Green circle
Postprint: archiving allowed
Red circle
Published version: archiving forbidden
Data provided by SHERPA/RoMEO


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.