A Provably Correct Translation of the <i>λ</i>-Calculus into a Mathematical Model of C plus

作     者：Rauf, Rose H. Abdul Berger, Ulrich Setzer, Anton 

作者机构：Univ Teknol MARA Fac Informat Syst & Quantitat Sci Shah Alam 40450 Selangor De Malaysia Univ Wales Swansea Dept Comp Sci Swansea SA2 8PP W Glam Wales 

出 版 物：《THEORY OF COMPUTING SYSTEMS》 (Theory Comput. Syst.)

年 卷 期：2008年第43卷第3-4期

页      面：298-321页

核心收录：

学科分类：07[理学] 0701[理学-数学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 070101[理学-基础数学] 

基　　金：Engineering and Physical Sciences Research Council  EPSRC  (GR/S30450/01) 

主　　题：Functional programming Object-oriented programming Inheritance Simply typed lambda-calculus Denotational semantics Kripke-style logical relation Correctness proof 

摘      要：We introduce a translation of the simply typed lambda-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 lambda-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 lambda-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.