1Team

• INRIA
  • Manuel Serrano (Manuel.Serrano@inria.fr)
  • Gerard Boudol (Gerard.Boudol@inria.fr)
  • Florian Loitsch (Florian.Loitsch@inria.fr)
  • Bernard Serpette (Bernard.Serpette@inria.fr)
  • Cyprien Nicolas (Cyprien.Nicolas@inria.fr)
• LIP6
  • Christian Queinnec (Christian.Queinnec@lip6.fr)
  • Emmanuel Chailloux (Emmanuel.Chailloux@lip6.fr)
  • Benjamin Canou (Benjamin.Canou@lip6.fr)
  • Vivien Ravet (Vivien.Ravet@lip6.fr)
• PPS
  • VIncent Balat (vincent.balat@pps.jussieu.fr)
  • Jérôme Vouillon (vouillon@pps.jussieu.fr)

2Software

We develop new software programs for the Web. They are available online on the dedicated web sites:

• Hop: http://hop.inria.fr
• Ocsigen: http://ocsigen.org
• Obrowser: http://www.pps.jussieu.fr/~canou/obrowser/tutorial

21Software releases

Since the beginning of the ANR PWD project, several versions of HOP, Ocsigen, and Obrowser have been publicly released. The main releases have been:

1. hop-1.11.0 released September 2009.
2. ocsigen-1.2.1 released September 2009.
3. ocsigen-1.3.1 released April 2010.
4. hop-2.0.0 released May 2010.
5. hop-2.1.0 released August 2010.
6. hop-2.2.0 released January 2011.
7. obrowser-1.1.1 released April 2011.

The new major release hop-2.3.0 is planned for October 2011, the new release ocsigen-2.0.0 is due by the end of the autumn.

3New results

31Hss: a Compiler for Cascading Style Sheets

The article 5 presents HSS, a compiler for CSS. It is first argued that generating CSS improves portability and maintainability of CSS files. This claim is supported by realistic examples. Then, the HSS compilation algorithm is presented. It is simple enough to be easily adapted to most web development kits.

HSS can be used as a stand-alone HSS-to-CSS compiler in the goal of enriching CSS with user defined variables, functions, and element types. It can also be used with the Hop web development kit in which case, working hand in hand with the Hop programming language, it can be used to implement skinning or theming of web applications.

32Towards Reasoning for Web Applications: An Operational Semantics for Hop

We propose 2 a small-step operational semantics to support reasoning about web applications written in the multi-tier language HOP. The semantics covers both server side and client side computations, as well as their interactions, and includes creation of web services, distributed client-server communications, concurrent evaluation of service requests at server side, elaboration of HTML documents, DOM operations, evaluation of script nodes in HTML documents and actions from HTML pages at client side.

33A multi-tier semantics for Hop

Hop is a multi-tier programming language where the behavior of interacting servers and clients are expressed by a single program. Hop adheres to the standard web programming style where servers elaborate HTML pages containing JavaScript code. This JavaScript code responds locally to user's interactions but also (following the so-called Ajax style) requests services from remote servers. These services bring back new HTML fragments containing additional JavaScript code replacing or modifying the state of the client.

The paper 7 presents a continuation-based denotational semantics for a sequential subset of Hop. Though restricted to a single server and a single client, this semantics takes into account the key feature of Hop namely that the server elaborates client code to be run in the client's browser. This new client-code dynamically requests services from the server which, again, elaborate new client code to be run in the client's browser.

This semantics details the programming model advocated by Hop and provides a sound basis for future studies such as security of web applications and web continuations.

34Automated Code Injection Prevention for Web Applications

We study common security problems related to integrity violations in web applications. We are interested in providing formal bases to prove that web applications's (and more generally generated mashups's)

- trusted components will be code injection free at run-time - untrusted components's influence to trusted components is limited to a set of given authorized resources.

We investigate formalization of these properties by means of web applications abstract semantics and discuss correct implementations to enforce them. We have incorporated the proposed enforcement mechanisms as additional modular compilation stages in HOP, a full-fledged multi-tier language to write web applications. This work is presented in 4.

35HopTeX - Compiling HTML to LaTeX with CSS

The article 6 presents HopTeX, a new application for authoring Html and LaTeX documents. The content of the document can is either be expressed in Html or in a blending of Html and a dedicated wiki syntax, for the sake of conciseness and readability. The rendering of the document is expressed by a set of CSS rules. The main originality of HopTeX is to consider LaTeX as a new media type for Html and to express the compilation from Html to LaTeX by the means of dedicated style sheet rules.

HopTeX can then be used to generate high quality documents for both paper printed version and electronic version. The online version of this paper is available at the HopTeX web page. It can be read using a regular Web browser or using Smartphone browsers.

HopTeX is implemented in HOP, a multi-tier programming language for the Web 2.0. This implementation extensively relies on two facilities generally only available on the client-side that HOP also supports on the server-side of the application: DOM manipulations and CSS server-side resolutions.

36Type-safe document manipulations

As part of Benjamin Canou's thesis 1, we proposed a high level and type-safe API for document manipulations. The goal was to be safer and more high-level than the browser's DOM. In particular, we aimed at eliminating the implicit moves performed by the DOM to maintain the tree structure which limit the possibilities of static typing.

First, we gave a minimal formal model similar to the DOM. Upon this first model, we built an alternative document API in which moves are replaced by implicit deep copy operations.

To prove the validity of our approach, we designed on top of this document API a language based on ML equiped with document manipulation features, that are well typed thanks to the use of our alternative document model.

An implementation of the language is ongoing, and scientific publications are to be submitted soon.

37Rethinking Web interaction

Paper submitted.

Web sites are evolving into ever more complex distributed applications. But current Web programming tools are not fully adapted to this evolution, and force programmers to worry about too many inessential details. We want to define an alternative programming style better fitted to that kind of applications. To do that, we propose an analysis of Web interaction in order to break it down into very elementary notions, based on semantic criteria instead of technological ones. This allows defining a common vernacular language to describe the concepts of current Web programming tools, but also some other new concepts. We use this to define a new service identification mechanism.

This results in a significant gain of expressiveness. The understanding and separation of these notions also makes it possible to get strong static guarantees, that can help a lot during the development of complex applications, for example by making impossible the creation of broken links. Most of the ideas we propose have been implemented in the Ocsigen Web programming framework. We give a quick outline of that implementation.

38From Bytecode to Javascript: the Js_of_ocaml Compiler

Paper submitted.

We present the design and implementation of a compiler from OCaml bytecode to Javascript. We believe that taking bytecode as input instead of a high-level language is a sensible choice. Virtual machines provide a very stable API. Such a compiler is thus easy to maintain. It is also convenient to use: it can just be added to an existing installation of the development tools. Already compiled libraries can be used directly, with no need to reinstall anything. Finally, some virtual machines are the target of several languages. A bytecode to Javascript compiler would make it possible to retarget all these languages to Web browsers at once.

4Dissemination

1. M. Serrano and C. Queinnec published a tutorial about Hop in the French magazine Gnu Linux France 8.
2. M. Serrano gave a presentation about Hop at the Collège de France in February 2010. The video is available at http://www.college-de-france.fr.
3. M. Serrano gave a talk about Diffuse Systems in the Seven Keys to the Digital Future seminar at the Royal Society of Edinburgh. See http://idea.ed.ac.uk/future.
4. M. Serrano gave a presentation of diffuse computing colloqium given in the honor of Jean-Jacques Levy and Gérard Berry. See http://www.lri.fr/~conchon/gerardmer.
5. M. Serrano gave a presentation of Hop at the Microsoft Software Summit that took place in Paris in April 2011. See http://research.microsoft.com/en-us/um/cambridge/events/ss2011.

5Meetings

51Kick off meeting (21 Jan 2010, Paris)

The kick off meeting took place at the University Pierre et Marie Curie.

511Participants

• PPS: Vincent Balat, Jérôme Vouillon
• LIP6: Christian Queinnec, Benjamin Canou
• INRIA: Manuel Serrano
• Invités: Frédéric Boussinot (INRIA)

512Introduction

• PPS: new interaction models for the web 2.0.
  • Ocsigen will be multi-tier in 1 months (Ocsigen 2.0)
  • Current release 1.3.0 (OcsigenServer + Elium + Oxymore)
• LIP6 + PPS:
  • O'Browser 1.1
  • environment: typed DOM and semantics of the DOM.
• LIP6 + INRIA:
  • Denotational semantics for Hop
  • Semantics of the client-side code generation
• INRIA:
  • Hop ported to Maemo
  • Integrate security policies in the client-code generator

513Talks and demonstrations

• Frédéric Boussinot has presented FunLoft (cooperation + asynchronous programming).
• Benjamin Canou gave a demonstration of O'Browser (client-side games using the HTML5 Canvas). Performance evaluation: about 10 times slower than JavaScript.
• Jérôme Vouillon gave a talk about the Lightweight Threads in OCaml
  • cooperative threads
  • monadic threads

52Second plenary meeting (17 sep 2010, Paris)

521Participants

• PPS: Vincent Balat, Jérôme Vouillon
• LIP6: Christian Queinnec, Emmanuel Chailloux, Benjamin Canou, Gégoire Henry
• INRIA: Manuel Serrano

522Talks and demonstrations

• Manuel Serrano gave a talk about HSS, a compiler for CSS and a short demonstration of HopTeX, a HOP to TeX compiler.
• Grégoire Henry gave a talk on Safe serialization in OCaml 3.
• Vincent Balat presented a survey of server-side programming with Eliom.

53Third plenary meeting (22 jun 2011, Paris)

531Participants

• PPS: Vincent Balat, Jérôme Vouillon, Mikael Laporte (Master student M1) Pierre Chambart (post doc)
• LIP6: Emmanuel Chailloux, Jeremy Salvucci (Master student), Benjamin Canou (PhD), Christian Queinnec (excused)
• INRIA: Manuel Serrano

532Talks and demonstrations

• Manuel Serrano gave a survey on programming with Hop.
• Jérôme Vouillon gave a presentation of js_of_ocaml, a Ocaml bytecode to JS compiler.
• Benjamin Canou gave a survey on multi-tiers programming languages.

6References