A Provably Correct Translation of the λ-Calculus into a Mathematical Model of C++ | Zendy

Rose H. Abdul Rauf | Zendy; Ulrich Berger | Zendy; Anton Setzer | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Provably Correct Translation of the λ-Calculus into a Mathematical Model of C++

Author(s) -

Rose H. Abdul Rauf,

Ulrich Berger,

Anton Setzer

Publication year - 2007

Publication title -

theory of computing systems

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.479

H-Index - 44

eISSN - 1433-0490

pISSN - 1432-4350

DOI - 10.1007/s00224-007-9062-1

Subject(s) - fragment (logic) , correctness , denotational semantics , translation (biology) , completeness (order theory) , computer science , semantics (computer science) , calculus (dental) , normalisation by evaluation , programming language , algebra over a field , operational semantics , mathematics , pure mathematics , medicine , mathematical analysis , biochemistry , chemistry , dentistry , messenger rna , gene

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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research