inria > sophia
Indes
Informatique Diffuse et Sécurisée
-- Publications





Classified publications


Chronological bibliography

2012

2011

2010

[GM10]Gazagnaire, T. and Madhavapeddy, A. -- Statically-typed value persistence for ML -- Proceedings of the Workshop on Generative Technologies (WGT'2010), Paphos, Cyprus, March, 2010.
[Pet10]Petri, G. -- Operational Semantics of Relaxed Memory Models -- Université de Nice - Sophia Antipolis, November, 2010.
[Ser10]Serrano, M. -- HSS: a Compiler for Cascading Style Sheets -- 12th Sigplan Int'l Conference on Principles and Practice of Declarative Programming (PPDP), Hagenberg, Austria, Jul, 2010.
[ pdf ]
This article 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.
[BLR10]Boudol, G. et al. -- Towards Reasoning for Web Applications: an Operational Semantics for Hop -- Proceedings of the first Workshop on Analysis and Programming Languages for Web Applications and Cloud Applications (APLWACA'10), Toronto, Canada, Jun, 2010.
[ pdf ]
We propose 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.
[Chr10]Christian Queinnec, -- An Infrastructure for Mechanised Grading -- CSEDU 2010 -- Proceedings of the second International Conference on Computer Supported Education, Valencia, Spain, Apr, 2010, pp. 37--45.
[ http://hal.archives-ouvertes.fr/hal-00429671/fr/ ]
Mechanised grading is now mature. In this paper, we propose elements for the next step: building a commodity infrastructure for grading. We propose --- an architecture for a grading component able to be embedded into various learning environments, --- a set of extensible Internet-based protocols to interact with this component, and --- a self-contained file format to thoroughly define an exercise in order to ease deployment. The infrastructure was designed to be scalable, robust and secure. First experiments with a partial implementation of this platform show the versatility and the neutrality of the grading component. It does not impose any IDE and it respects the tenets of the embedding learning environment or course-based system.
[SQ10]Serrano, M. and Queinnec, C. -- HTML5 Video portable avec Heb -- Jan, 2010.
[ http://www.programmez.com ]
[LRS10]Luo, Z. and Rezk, T. and Serrano, M. -- Automated Code Injection Prevention for Web Applications -- Submitted, 2010.
[SSG10]Scott, D. et al. -- Using functional programming within an industrial product group: perspectives and perceptions -- Proceedings of the 15th ACM SIGPLAN international conference on Functional programming, ICFP '10, Baltimore, Maryland, USA, 2010, pp. 87--92.
[ http://doi.acm.org/10.1145/1863543.1863557 ]
[Bou10]Boussinot, F. -- The FunLoft Language -- http://hal.archives-ouvertes.fr/inria-00497705, 2010.
[ http://hal.archives-ouvertes.fr/inria-00497705 ]
[Bou10b]Boudol, G. -- Typing termination in a higher-order concurrent imperative language -- Information and Computation, 2082010, pp. 716-736.
[BP10]Boudol, G. and Petri, G. -- A Theory of Speculative Computation -- ESOP, Paphos, Cyprus, 2010, pp. 165-184.
[SQ10b]Serrano, M. and Queinnec, C. -- A multi-tier semantics for Hop -- Higher Order and Symbolic Computation (HOSC), 2010.
Hop is a multi-tier programming language where a single program specifies servers and clients behaviors altogether. 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.This paper 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 nature of the web where the server elaborates some JavaScript code to be run in the client's browser. This new client-code dynamically requests services from the server which, again, elaborate new JavaScript 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 web continuations and concurrency.
[Ser10b]Serrano, M. -- HopTeX - Compiling HTML to LaTeX with CSS -- Submitted, 2010.
[MMS10]Madhavapeddy, A. et al. -- Turning down the LAMP: software specialisation for the cloud -- Proceedings of the 2nd USENIX conference on Hot topics in cloud computing, HotCloud'10, Boston, MA, 2010, pp. 11--11.
[ http://portal.acm.org/citation.cfm?id=1863103.1863114 ]
[BDR10]Barthe, G. and D'Argenio, P. and Rezk, T. -- Secure Information Flow by Self Composition -- Special Issue of MSCS of PLID, 2010.
[Ber10]Berry, G. -- Penser, modéliser et maîtriser le calcul informatique, notes de cours -- Collège de France, 2010.
[Bou10c]Boussinot, F. -- Safe Reactive Programming - The FunLoft Language -- Lambert Academic Pub., 2010.
[BRR10]Barthe, G. et al. -- Security of Multithreaded Programs by Compilation -- ESORICS'07 Special Issue in ACM Transactions on Information and System Security (TISSEC), 2010.
[GM10b]Gazagnaire, T. and Madhavapeddy, A. -- Dynamics for ML using Meta-Programming -- Electonic Notes in Theoritical Computer Science, 2010.
[CCD10]Capecchi, S. et al. -- Session Types for Access and Information Flow Control -- Inria, 2010.
We consider a calculus for multiparty sessions with delegation, enriched with security levels for session participants and data. We propose a type system that guarantees both session safety and a form of access control. Moreover, this type system ensures secure information flow, including controlled forms of declassification. In particular, it prevents leaks due to the specific control constructs of the calculus, such as session opening, selection, branching and delegation. We illustrate the use of our type system with a number of examples, which reveal an interesting interplay between the constraints of security type systems and those used in session types to ensure properties like communication safety and session fidelity.
[Ber10b]Berry, G. -- Seven Keys to the Digital Future -- Available at http://idea.ed.ac.uk/future/, 2010.
[CCD10b]Capecchi, S. et al. -- Session Types for Access and Information Flow Control -- CONCUR'10, Lecture Notes in Computer Science, 2010, pp. 237-252.
[G. 10]G. Berry, -- Seven Keys to the Digital Future -- Textes et documents pour la classe, (997), 2010.
[Ber10c]Berry, G. -- Penser, modéliser et maîtriser le calcul informatique, vidéos -- Available at http://www.college-de-france.fr/default/EN/all/cha, 2010.
[BHL10]Barthe, G. et al. -- Robustness Guarantees for Anonymity -- CSF, 2010, pp. 91-106.


This Html page has been produced by Skribe.
Last update Thu Jul 7 08:23:54 2011.