A Provably Correct Translation of the λ -Calculus into a Mathematical Model of C++
2008
We introduce a translation of the simply typed λ-calculus into C++, and give a mathematical proof of the correctness of this translation. For this purpose we develop a suitable fragment of C++ together with a denotational semantics. We introduce a formal translation of the λ-calculus into this fragment, and show that this translation is correct with respect to the denotational semantics. We show as well a completeness result, namely that by translating λ-terms we obtain essentially all C++ terms in this fragment. We introduce a mathematical model for the evaluation of programs of this fragment, and show that the evaluation computes the correct result with respect to this semantics.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
51
References
0
Citations
NaN
KQI