A provably correct compilation of functional languages into scripting languages

DOI10.7561/SACS.2017.1.19zbMATH Open1424.68028MaRDI QIDQ4621210FDOQ4621210

Authors Paola Giannini, Albert Shaqiri

Publication date 8 February 2019

Published in Scientific Annals of Computer Science (Search for Journal in Brave)

zbMATH Keywords

functional languagesscripting languagesintermediate languagecorrect translation

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18)

Recommendations

• Fully abstract compilation to JavaScript
• scientific article; zbMATH DE number 2079040
• A provably correct translation of the \(\lambda \)-calculus into a mathematical model of C++
• A verified compiler for an impure functional language
• Functional runtime systems within the lambda-sigma calculus

Cited in

(5)

• An implementation of syntax directed functional programming on nested- stack machines
• Skribe: a functional authoring language
• The correctness of a code generator for a functional language
• A provably correct translation of the \(\lambda \)-calculus into a mathematical model of C++
• Observational program calculi and the correctness of translations

Describes a project that uses

Uses Software

• Isabelle/HOL
• JavaScript
• Featherweight Java
• Python
• F#

This page was built for publication: A provably correct compilation of functional languages into scripting languages

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4621210)