publication . Part of book or chapter of book . Under curation

The Correctness of a Code Generator for a Functional Language

Courant, Nathanaël; Séré, Antoine; Shankar, Natarajan;
Open Access
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 bi...
Download from
ZENODO
Part of book or chapter of book
Provider: ZENODO
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue