@inproceedings{10.1145/2429069.2429114,
author = {Fournet, Cedric and Swamy, Nikhil and Chen, Juan and Dagand, Pierre-Evariste and Strub, Pierre-Yves and Livshits, Benjamin},
title = {Fully Abstract Compilation to JavaScript},
year = {2013},
isbn = {9781450318327},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2429069.2429114},
doi = {10.1145/2429069.2429114},
abstract = {Many tools allow programmers to develop applications in high-level languages and deploy them in web browsers via compilation to JavaScript. While practical and widely used, these compilers are ad hoc: no guarantee is provided on their correctness for whole programs, nor their security for programs executed within arbitrary JavaScript contexts. This paper presents a compiler with such guarantees. We compile an ML-like language with higher-order functions and references to JavaScript, while preserving all source program properties. Relying on type-based invariants and applicative bisimilarity, we show full abstraction: two programs are equivalent in all source contexts if and only if their wrapped translations are equivalent in all JavaScript contexts. We evaluate our compiler on sample programs, including a series of secure libraries.},
booktitle = {Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {371–384},
numpages = {14},
keywords = {program equivalence, refinement types, full abstraction},
location = {Rome, Italy},
series = {POPL '13}
}