Program
of
trackWeb Programming

List of accepted papers :

• Invited talk: Static Analysis Challenges in Web Programming
  Authors: X. Rival

• Tierless Web programming in the large
  Authors: Gabriel Radanne and Jérôme Vouillon

  Keywords: Web, client/server, OCaml, ML, Eliom, functional, module, separate compilation

  Abstract:
  Tierless Web programming languages allow to combine client-side, and server-side programming in a single program. This allows to, define expressions with both client and server parts, and at the, same time provides good static guarantees regarding client-server, communication. However, these nice properties come at a cost:, most tierless languages offer very poor support for modularity and, separate compilation., To regain this modularity and offer a larger-scale notion of com-, position, we propose to leverage a well-known tool: ML-style mod-, ules. In modern ML languages, the module system is a layer separate, from the expression language., Eliom is an extension of OCaml for tierless Web programming, which provides type-safe communication and an efficient execution, model. In this article, we present how the Eliom module system, combines the flexibility of tierless Web programming languages, with a powerful module systems, thus providing good support for, abstraction, modularity and separate compilation. We also show, that we can provide all these advantages while providing seamless, integration with OCaml and its ecosystem.

• JSExplain: a Double Debugger for JavaScript
  Authors: Arthur Charguéraud, Alan Schmitt and Thomas Wood

  Keywords: javascript, ocaml, interpreter, debugger, semantics

  Abstract:
  We present JSExplain, a reference interpreter for JavaScript that closely follows the specification and that produces execution traces. These traces may be interactively investigated in a browser, with an interface that displays not only the code and the state of the interpreter, but also the code and the state of the interpreted program. Conditional breakpoints may be expressed with respect to both the interpreter and the interpreted program. In that respect, JSExplain is a double-debugger for the specification of JavaScript.

• FAUST Domain Specific Audio DSP language compiled to WebAssembly
  Authors: Stéphane Letz, Yann Orlarey and Dominique Fober

  Keywords: Signal processing, Domain Specific Language, audio, Faust, DSP, compilation, WebAssembly, WebAudio

  Abstract:
  This paper demonstrates how FAUST, a functional programming language for sound synthesis and audio processing, can now be used to develop efficient audio nodes for the Web. After a brief introduction of the language, the generation of WebAssembly code and the deployment of specialized WebAudio nodes will be explained. Several use cases will be presented. Extensive benchmarks to compare the performances of native and WebAssembly versions of the same set of DSP have be done and will be commented.

• Language-integrated queries: a BOLDR approach
  Authors: Véronique Benzaken, Giuseppe Castagna, Laurent Daynes, Julien Lopez, Kim Nguyen and Romain Vernoux

  Keywords: databases, language runtimes, language integrated queries, dynamic languages

  Abstract:
  We present BOLDR, a modular framework that enables the evaluation in, databases of queries containing application logic and, in particular,, user-defined functions. BOLDR also allows the nesting of queries for different, databases of possibly different data models. The framework detects the, boundaries of queries present in an application, translates them into an, intermediate representation together with the relevant language environment,, rewrites them in order to avoid query avalanches and to make the most out of, database optimizations, and converts the results back to the application. We, also present experiments showing that the techniques we implemented are, applicable to real-world database applications, both in terms of successfully, handling different sorts of language-integrated queries, and in terms of, better performance.

• PixieDust: Declarative Incremental User Interface Rendering through Static Dependency Tracking
  Authors: Nick ten Veen, Daco Harkes and Eelco Visser

  Keywords: User Interface, Incremental Computing, Reactive Programming

  Abstract:
  Modern web applications are interactive., Reactive programming languages and libraries are the state-of-the-art approach for declaratively specifying these interactive applications., However, programs written with these approaches contain error-prone boilerplate code for efficiency reasons., , In this paper we present PixieDust, a declarative user-interface language for browser-based applications., PixieDust uses static dependency analysis to incrementally update a browser-DOM at runtime, without boilerplate code., We demonstrate that applications in PixieDust contain less boilerplate code than state-of-the-art approaches, while achieving on-par performance.

• A Better Facet of Dynamic Information Flow Control
  Authors: Minh Ngo, Nataliia Bielova, Cormac Flanagan, Tamara Rezk, Alejandro Russo and Thomas Schmitz

  Keywords: Multiple Facets, Dynamic Information Flow Control, Non-Interference, Secure Multi-Execution

  Abstract:
  Multiple Facets (MF) is a dynamic enforcement mechanism which has proved to be a good fit for implementing information flow security for JavaScript. It relies on multi executing the program, once per each security level or view, to achieve soundness. By looking inside programs, MF encodes the views to reduce the number of needed multi-executions., , In this work, we extend Multiple Facets in three directions. First, we propose a new version of MF for arbitrary lattices, called Generalised Multiple Facets, or GMF. GMF strictly generalizes MF, which was originally proposed for a specific lattice of principals. Second, we propose a new optimization on top of GMF that further reduces the number of executions. Third, we strengthen the security guarantees provided by Multiple Facets by proposing a termination sensitive version that eliminates covert channels due to termination.

• A Formal Semantics of the Core DOM in Isabelle/HOL
  Authors: Achim D. Brucker and Michael Herzberg

  Keywords: Document Object Model, DOM, Formal Semantics, Standard Conformance Testing, Isabelle/HOL

  Abstract:
  At its core, the Document Object Model (DOM) defines a tree-like data structure for representing documents in general and HTML documents in particular. It forms the heart of any rendering engine of modern web browsers. Formalizing the key concepts of the DOM is a pre-requisite for the formal reasoning over client-side JavaScript programs as well as for the analysis of security concepts in modern web browsers. In this paper, we present a formalization of the core DOM, with focus on the node-tree and the operations defined on node-trees, in Isabelle/HOL. We use the formalization to verify the functional correctness of the most important functions defined in the DOM standard. Moreover, our formalization is (1) extensible, i.e., can be extended without the need of re-proving already proven proper- ties and (2) executable, i.e., we can generate executable code from our specification. Finally, we present an approach for showing the conformance of our formalization to the official DOM standard by translating test cases from the official standard developers into proof obligations in our formal model.