sign in
english version rss feed

hal-00780803, version 1

Fully Abstract Compilation to JavaScript

Cédric Fournet () 1, Nikhil Swamy () 2, Juan Chen () 2, Pierre-Evariste Dagand (, https://personal.cis.strath.ac.uk/pierreevariste.dagand/index.html) 2, Pierre-Yves Strub (, http://pierre-yves.strub.nu/) 3, Benjamin Livshits () 2

40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL'13 (2013) (2013)

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.

  • Domain : Computer Science/Programming Languages
    Computer Science/Logic in Computer Science
 
  • hal-00780803, version 1
  • oai:hal.inria.fr:hal-00780803
  • From: 
  • Submitted on: Thursday, 24 January 2013 18:50:09
  • Updated on: Friday, 25 January 2013 10:49:04
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...