A Provably Correct Compilation of Functional Languages into Scripting Languages

Published in Volume XXVII, Issue 1, 2017, pages 19-76, doi: 10.7561/SACS.2017.1.19

Authors: P. Giannini, A. Shaqiri

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

Full Text (PDF)

References

[1] D. Ancona, P. Giannini, and E. Zucca. Reconciling positional and nominal binding. In Proceedings of the Sixth Workshop on Intersection Types and Related Systems (ITRS’12), Dubrovnik, Croatia, 29th June 2012, volume 121 of EPTCS, pages 81–93, 2012. doi:10.4204/EPTCS.121.6.

[2] D. Ancona, P. Giannini, and E. Zucca. Incremental Rebinding. In Proceedings of the 14th Italian Conference on Theoretical Computer Science (ICTCS’13). http://www.di.unito.it/˜giannini/papers/ICTCS13.pdf 2013.

[3] A.W. Appel. Compiling with Continuations. Cambridge University Press, 1992.

[4] A.W. Appel. Modern Compiler Implementation in ML. Cambridge University Press, 1998.

[5] N. Benton and C.-K. Hur. Biorthogonality, step-indexing and compiler correctness. In Graham Hutton and A.P. Tolmach, editors, Proceedingsof the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 – September 2, 2009, pages 97–108. ACM, 2009. doi:10.1145/1596550.1596567.

[6] Z. Bray, T. Petříček, R. Pickering, and J. Freiwirth. Funscript. http://funscript.info/, February 2013.

[7] M.A. Dave. Compiler verification: A bibliography. ACM SIGSOFT Software Engineering Notes, 28(6):2–2, November 2003. doi: 10.1145/966221.966235.

[8] I. Elliot. Pit – F# to JavaScript compiler. http://www.i-programmer.info/news/167-javascript/3678-pit-f-to-javascript-compiler.html, 2012.

[9] C. Flanagan, A. Sabry, B.F. Duba, and M. Felleisen. The essence of compiling with continuations. In Robert Cartwright, editor, Proceedings of the ACM SIGPLAN’93 Conference on Programming Language Design and Implementation (PLDI), Albuquerque, New Mexico, USA, June 23-25, 1993, pages 237–247. ACM, 1993. doi:10.1145/155090.155113.

[10] M. Fluet and S. Weeks. Contification using dominators. In Benjamin C. Pierce, editor, Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP ’01), Firenze (Florence), Italy, September 3-5, pages 2–13. ACM, 2001. doi:10.1145/507635.507639.

[11] C. Fournet, N. Swamy, Juan Chen, P.-E´ . Dagand, P.-Y. Strub, and B. Livshits. Fully abstract compilation to JavaScript. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 371–384. ACM, 2013. doi:10.1145/2480359.2429114.

[12] P. Giannini and A. Shaqiri. An intermediate language for compilation to scripting languages. In Jos´e Cordeiro, David A. Marca, and Marten van Sinderen, editors, ICSOFT 2013 – Proceedings of the 8th International Joint Conference on Software Technologies, Reykjav´ık, Iceland, pages 92–103. SciTePress, 2013. doi:10.5220/0004588600920103.

[13] P. Giannini and A. Shaqiri. Blue Storm Compiler. https://www.assembla.com/spaces/bluestorm, 2014.

[14] P. Giannini and A. Shaqiri. Compiling functional to scripting languages. Communications in Computer and Information Science, 457:114–130, 2014. doi:10.1007/978-3-662-44920-2_8.

[15] A. Igarashi, B. Pierce, and P. Wadler. Featherweight Java: A minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems, 23(3):396–450, 2001. doi:10.1145/503502.503505.

[16] Intellifactory. Websharper 2010 platform. http://websharper.com/, May 2012.

[17] A. Kennedy. Compiling with continuations, continued. In Ralf Hinze and Norman Ramsey, editors, Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, October 1-3, 2007, pages 177–190. ACM, 2007. doi:10.1145/1291151.1291179.

[18] R. Kumar, M.O. Myreen, M. Norrish, and S. Owens. Cakeml: a verified implementation of ML. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, pages 179–192. ACM, 2014. doi: 10.1145/2535838.2535841.

[19] X. Leroy and H. Grall. Coinductive big-step operational semantics. Information and Computation, 207(2):284–304, 2009. doi: 10.1016/j.ic.2007.12.004.

[20] T. Petříček and D. Syme. AFAX: Rich client/server web ap- plications in F#. http://www.scribd.com/doc/54421045/Web-Apps-in-F-Sharp, May 2012.

[21] J.F. Ranson, H.J. Hamilton, and P.W. L. Fong. A semantics of Python in Isabelle/HOL. Technical Report CS-2008-04, CS Department, University of Regina,Saskatchewan, 2008. URL: http://www.cs.uregina.ca/Research/Techreports/2008-04.pdf.

[22] J. Vouillon and V. Balat. From bytecode to JavaScript: the Js of ocaml compiler. Software: Practice and Experience, 44(8):951–972, 2014. doi:10.1002/spe.2187.

Bibtex

@article{sacscuza:giannini2017apccoflisl,
  title={A Provably Correct Compilation of Functional Languages into Scripting Languages},
  author={P. Giannini and A. Shaqiri},
  journal={Scientific Annals of Computer Science},
  volume={27},
  number={1},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  year={2017},
  pages={19--76},
  doi={10.7561/SACS.2017.1.19},
  publisher={``A.I. Cuza'' University Press}
}