A provably correct compilation of functional languages into scripting languages

Paola Giannini, Albert Shaqiri

Risultato della ricerca: Contributo su rivistaArticolo in rivistapeer review

Abstract

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 big-step 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.

Lingua originaleInglese
pagine (da-a)19-76
Numero di pagine58
RivistaScientific Annals of Computer Science
Volume27
Numero di pubblicazione1
DOI
Stato di pubblicazionePubblicato - 2017

Fingerprint

Entra nei temi di ricerca di 'A provably correct compilation of functional languages into scripting languages'. Insieme formano una fingerprint unica.

Cita questo