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 JS. 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 JS contexts. This paper presents a compiler with such guarantees. We compile an ML-like language with higher-order functions and references to JS, 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 JS contexts. We evaluate our compiler on sample programs, including a series of secure libraries.
Type de document :
Communication dans un congrès
40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL'13 (2013), Jan 2013, Roma, Italy. 2013
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00780803
Contributeur : Pierre-Yves Strub <>
Soumis le : jeudi 24 janvier 2013 - 18:50:09
Dernière modification le : jeudi 5 février 2015 - 16:26:02
Document(s) archivé(s) le : samedi 1 avril 2017 - 10:12:05

Fichier

js-star-popl-2013.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00780803, version 1

Collections

Citation

Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Evariste Dagand, Pierre-Yves Strub, et al.. Fully Abstract Compilation to JavaScript. 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL'13 (2013), Jan 2013, Roma, Italy. 2013. 〈hal-00780803〉

Partager

Métriques

Consultations de la notice

407

Téléchargements de fichiers

327