A Provably Correct Compilation of Functional Languages into Scripting Languages

Scientific Annals of Computer Science

article

P. Giannini¹  A. Shaqiri² 

[1] Universit`a del Piemonte Orientale, DiSIT;Dipartimento di Informatica, Universit`a degli Studi di Milano

关键词: functional languages;    scripting languages;    correct translation;    intermediate language;   

DOI  :  10.7561/SACS.2017.1.19

来源: Alexandru Ioan Cuza University of Iasi

【 摘 要 】

In this paper we consider the problem of translating core F#, a typed functional language including mutable variables and exception handling, into scripting languages such as JavaScript or Python. In previous work, we abstracted the most significant characteristics of scripting languages in an intermediate language (IL for short). IL is a block-structured imperative language in which a definition of a name does not have to statically precede its use. We define a bigstep operational semantics for core F# and for IL and formalise the translation of F# expressions into IL. The main contribution of the paper is the proof of correctness of the given translation, which is done by showing that the evaluation of a well-typed F# program converges to a primitive value if and only if the evaluation of its translation into IL converges to the same value.

【 授权许可】

CC BY-ND