@inproceedings{f9582560ac694e47bf3418edacec0c04,
title = "Fully abstract compilation to JavaScript",
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.",
keywords = "full abstraction, program equivalence, refinement types",
author = "C{\'e}dric Fournet and Nikhil Swamy and Juan Chen and Dagand, \{Pierre Evariste\} and Strub, \{Pierre Yves\} and Benjamin Livshits",
year = "2013",
month = feb,
day = "26",
doi = "10.1145/2429069.2429114",
language = "English",
isbn = "9781450318327",
series = "Conference Record of the Annual ACM Symposium on Principles of Programming Languages",
pages = "371--383",
booktitle = "POPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",
note = "40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013 ; Conference date: 23-01-2013 Through 25-01-2013",
}