
Here is our classified list of publications:
Chronological bibliography

[Ser09]  Serrano, M.  Anatomy of a Ubiquitous Media Center  Proceedings of the Sixteenth Annual Multimedia Computing and Networking (MMCN'09), San Jose, CA, USA, Jan, 2009. 

 The Web is such a rich architecture that it is giving birth to new applications that were unconceivable only few years ago in the past. Developing these applications being different from developing traditional applications, generalist programming languages are not well suited. To help face this problem, we have conceived the HOP programming language whose syntax and semantics are specially crafted for programming Web applications. In order to demonstrate that HOP, and its SDK, can be used for implementing realistic applications, we have started to develop new innovative applications that extensively rely on the infrastructure offered by the Web and that use features unique to HOP. We have initiated this effort with a focus on multimedia applications.
Using HOP we have implemented a distributed audio system. It supports a flexible architecture that allows new devices to catch up with the application any time: a cell phone can be used to pump up the volume, a PDA can be used to browse over the available musical resources, a laptop can be used to select the output speakers, etc. This application is intrinsically complex to program because, i it is distributed (several different devices access and control shared resources such a music repositories and sound card controllers), ii it is dynamic (new devices may join or quit the application at any time), and iii it involves different heterogeneous devices with different hardware architectures and different capabilities. 

 
[BD08]  Boussinot, F. and Dabrowski, F.  Safe Reactive Programming: the FunLoft Proposal  Proc. of MULTIPROG  First Workshop on Programmability Issues for MultiCore Computers, January, 2008. 
 
[SQ08]  Serrano, M. and Queinnec, C.  Une galerie de photos sur le Web avec HOP  Programmez!, (105), Feb, 2008. 
 [ http://www.programmez.com ] 
 
[Epa08]  Epardaud, S.  ULM, un langage pour la mobilité  Thèse de doctorat d'université, Université de Nice, Nice, Jan, 2008. 
 
[SQ08b]  Serrano, M. and Queinnec, C.  Hop, un langage de programmation pour le Web  Programmez!, (104), Jan, 2008. 
 [ http://www.programmez.com ] 
 
[Bou08]  Boudol, G.  Typing safe deallocation  ESOP'08, Lecture Notes in Computer Science, 2008, pp. 116130. 
 
[Ser08]  Serrano, M.  Hop, a Fast Server for the Diffuse Web  2008. 
 
[Bou08b]  Boudol, G.  Secure information flow as a safety property  FAST'08, 2008. 
 
[BP08]  Boudol, G. and Petri, G.  Relaxed memory models: an operational approach  accepted for publication at POPL'09, 2008. 
 
[LS08]  Loitsch, F. and Serrano, M.  Trends in Functional Programming, ch. Hop ClientSide Compilation  Moraz M. T. editor, Seton Hall University, Intellect Bristol, UK/Chicago, USA, 2008, pp. 141158. 
 
[BCH08]  Boudol, G. et al.  Twenty Years on: Reflections on the CEDISYS Project. Combining True Concurrency with Process Algebra  Springer, 2008. 
 
[Bou08c]  Boudol, G.  On strong normalization and type inference in the intersection type discipline  Theoretical Computer Science, 398(1), 2008, pp. 6381. 
 
[Cas07]  Castellani, I.  Stateoriented noninterference for CCS  6322, INRIA, 10, 2007. 
 [ ] 
 
[Bou07]  Boudol, G.  Définition d'une machine abstraite pour ULM  Livrable D1.1, CRE 46136511, Juin, 2007. 
 
[BCM07]  Boudol, G. and Castellani, I. and Matos, A.  Définition d'un modèle formel de contr de flux d'informations confidentielles : cas du langage ULM  Livrable D1.2, CRE 46136511, Avril, 2007. 
 
[ABD07]  Amadio, R. and Boudol, G. and Dabrowski, F.  Définition de techniques de preuve de terminaison et de contr de complexité d'exécution de programmes  Livrable D1.1, CRE 46136511, Juin, 2007. 
 
[SG07]  Serrano, M. and Gallesio, E.  An Adaptive Package Management System for Scheme  Proceedings of the Second Dynamic Languages Symposium, Montréal, Québec, Canada, Oct, 2007. 
 [ html ] 

 This paper presents a package management system for the Scheme programming language. It is inspired by the Comprehensive Perl Archive Network (Cpan) and various GNU/Linux distributions. It downloads, installs, and prepares source codes for execution. It manages the dependencies between packages. The main characteristic of this system is its neutrality with respect to the various Scheme implementations. It is neutral with respect to the language extensions that each Scheme implementation proposes and with respect to the execution environment of these implementations. This allows the programmer to blend, within the same program, independent components which have been developed and tested within different Scheme implementations. ScmPkg is available at: http://hop.inria.fr/hop/scmpkg 

 
[Loi07]  Loitsch, F.  Exceptional Continuations in JavaScript  2007 Workshop on Scheme and Functional Programming, Freiburg, Germany, Sep, 2007. 
 
[Ser07]  Serrano, M.  Programming Web Multimedia Applications with Hop  Proceedings of the ACM Sigmm and ACM Siggraph conference on Multimedia, Best Open Source Software, Augsburg, Germany, Sep, 2007. 
 [ pdf ] 

 Hop is a new execution platform for running interactive and multimedia applications on the Web. It is aimed at executing applications such as Web agendas, Web galleries, Web music players, etc. Hop consists of: i) a new programming language specially designed for addressing the distributed aspects of Web programming, ii) a rich set of libraries for dealing with music files, sounds, pictures, photographs, etc., iii) a fullfledged Web server for executing the serverside components of the applications. In this paper we illustrate Hop's skills for programming multimedia applications in two examples. We show that, with 50 lines of code, an operational photograph gallery can be implemented and we show that with approximatively 30 lines of code an operational podcast receiver can be built. 

 
[AD07]  Amadio, R. and Dabrowski, F.  Feasible reactivity in a synchronous picalculus  Proceedings ACM SIGPLAN Principles and Practice of Declarative Programming , Jul, 2007, pp. 4555 . 
 
[AP07]  Amadio, R. and Phillips, I.  Proceedings of the 13th International Workshop on Expressiveness in Concurrency (EXPRESS 2006), Electronic Notes in Theoretical Computer Science, Volume 175(3).  Elsevier, Jun, 2007. 
 
[Ser07b]  Serrano, M.  The HOP platform  Invited presentation at the International Lisp Conference'07, Cambridge, UK, Jun, 2007. 
 
[Tar07]  Tardieu, O.  A deterministic logical semantics for pure Esterel  ACM Transactions on Programming Languages and Systems, 29(2), Apr, 2007, pp. 8. 
 
[LS07]  Loitsch, F. and Serrano, M.  Hop ClientSide Compilation  Proceedings of the 8th Symposium on Trends on Functional Languages, New Yort, USA, Apr, 2007. 
 [ http://cs.shu.edu/tfp2007/draftProcDocument.pdf  pdf ] 

 HOP is a new language for programming interactive Web applications. It aims to replace HTML, JavaScript, and serverside scripting languages (such as PHP, JSP, ...) with a unique language that unites clientside interactions and serverside computations. A HOP execution platform is made of two compilers. One that compiles the code executed by the server, and one that compiles the code executed by the client. T his paper presents the latter. In order to ensure compatibility of HOP graphical user interfaces with popular plain Web browsers, the clientside HOP compiler has to generate regular HTML and JavaScript code. Since the HOP language is built on top of the Scheme programming language, compiling HOP to JavaScript is nearly equivalent to compiling Scheme to JavaScript. The compiler we have designed supports the whole Scheme core language. In particular it optimizes tailrecursive calls. We show in this paper that this compiler is efficient because with optimizations for obvious tail recursive calls the generated code runs roughly at the same speed as equivalent handwritten JavaScript code. With support for all tail calls the generated code typically runs at most 2.1 times slower than without. The techniques presented in this paper can be applied to most strict functional languages such as ML and Lisp. 

 
[LS07b]  Loitsch, F. and Serrano, M.  Hop ClientSide Compilation  Proceedings of the 8th Symposium on Trends on Functional Languages, New York, USA, Apr, 2007. 
 [ http://cs.shu.edu/tfp2007/draftProcDocument.pdf  pdf ] 
 
[STE07]  Soviani, C. and Tardieu, O. and Edwards, S.  Optimizing Sequential Cycles through Shannon Decomposition and Retiming  IEEE Transactions on ComputerAided Design of Integrated Circuits and Systems, 26(3), Mar, 2007, pp. 456467. 
 
[TE07]  Tardieu, O. and Edwards, S.  Instantaneous Transitions in Esterel  Proceedings of the Workshop on ModelDriven HighLevel Programming of Embedded Systems, Braga, Portugal, Mar, 2007. 
 
[Ama07]  Amadio, R.  The SL synchronous language, revisited  Journal of Logic and Algebraic Programming , 70 Feb, 2007, pp. 121150 . 
 
[Dab07]  Dabrowsky, F.  Programmation Réactive Synchrone: langages et contrôle des ressources  Université Paris 7, 2007. 
 
[Bou07b]  Boussinot, F.  A Benchmark for Multicore Machines  http://hal.inria.fr/inria00174843, Inria, 2007. 
 
[BD07]  Boussinot, F. and Dabrowski, F.  Formalisation of FunLoft. http://hal.inria.fr/inria00183242  2007. 
 
[Ama07b]  Amadio, R.  A synchronous picalculus  Information and Computation. 205(9):14701490, 2007. 
 
[Bou07c]  Boudol, G.  Fair cooperative multithreading, or: typing termination in a higherorder concurrent imperative language  CONCUR'07, Lecture Notes in Computer Science, 2007, pp. 272286. 
 
[BD07b]  Boussinot, F. and Dabrowsky F.,  Formalisation of FunLoft  http://hal.inria.fr/inria00183242, Inria, 2007. 
 
[ABC07]  Almeida Matos, A. and Boudol, G. and Castellani, I.  Typing Noninterference for Reactive Programs  Journal of Logic and Algebraic Programming, 722007, pp. 124156. 
 
[Bou07d]  Boussinot, F.  A Benchmark for Multicore Machines. http://hal.inria.fr/inria00174843  2007. 
 
[BK07]  Boudol, G. and Kolundzija, M.  Access control and declassification  MMMACNS'07, Communications in Computer and Information Science, 2007. 
 
[Cas07b]  Castellani, I.  Stateoriented noninterference for CCS  ENTCS, 2007, pp. 3960. 
 [ ] 
 
[Alm06]  Almeida Matos, A.  Typing Secure Information Flow: Declassification and Mobility  École National Supérieure des Mines de Paris, January, 2006. 
 
[TE06]  Tardieu, O. and Edwards, S.  Schedulingindependent threads and exceptions in SHIM  Proceedings of the 6th ACM IEEE International conference on Embedded software, Seoul, Korea, Oct, 2006, pp. 142151. 
 
[Dam06]  Damien Ciabrini,  Débogage symbolique multilangages pour les platesformes d'exécution généralistes  Université de Nice Sophia Antipolis, Oct, 2006. 
 [ php?label=INRIA&action_todo=view&langue=en&id=tel00122789&version=1 ] 
 
[SGL06]  Serrano, M. and Gallesio, E. and Loitsch, F.  HOP, a language for programming the Web 2.0  Proceedings of the First Dynamic Languages Symposium, Portland, Oregon, USA, Oct, 2006. 
 [ html ] 
 
[SGL06b]  Serrano, M. and Gallesio, E. and Loitsch, F.  HOP, a language for programming the Web 2.0  Proceedings of the First Dynamic Languages Symposium, Portland, Oregon, USA, Oct, 2006. 
 [ html ] 

 Hop is a new higherorder language designed for programming interactive web applications such as web agendas, web galleries, music players, etc. It exposes a programming model based on two computation levels. The first one is in charge of executing the logic of an application while the second one is in charge of executing the graphical user interface. Hop separates the logic and the graphical user interface but it packages them together and it supports strong collaboration between the two engines. The two execution flows communicate through function calls and event loops. Both ends can initiate communications. The paper presents the main constructions of Hop. It sketches its implementation and it presents an example of a simple web application written in Hop. 

 
[Ser06]  Serrano, M.  The HOP Development Kit  Invited paper of the Seventh Acm sigplan Workshop on Scheme and Functional Programming, Portland, Oregon, USA, Sep, 2006. 
 [ html ] 

 Hop, is a language dedicated to programming reactive and dynamic applications on the web. It is meant for programming applications such as web agendas, web galleries, web mail clients, etc. While a previous paper (Hop, a Language for Programming the Web 2.0, available at http://hop.inria.fr) focused on the linguistic novelties brought by Hop, the present one focuses on its execution environment. That is, it presents Hop's user libraries, its extensions to the HTMLbased standards, and its execution platform, the Hop web broker. 

 
[ABC06]  Almeida Matos, A. and Boudol, G. and Castellani, I.  Typing Noninterference for Reactive Programs  2006. 
 
[RF06]  Roberto M. Amadio, and FréDéRic Dabrowski,  Feasible Reactivity in a synchronous picalculus, Draft  2006. 
 
[Van06]  Van Bakel, S.  The heart of intersection type assignment  RR5984, INRIA, 2006. 
 
[Ama06]  Amadio, R.  A synchronous picalculus  Université Paris 7, Laboratoire PPS, 2006. 
 
[AD06]  Amadio, R. and Dal Zilio, S.  Resource control for synchronous cooperative threads  Theoretical Computer Science, 3582006, pp. 229254. 
 
[ABB06]  Amadio, R. et al.  Reactive concurrent programming revisited  Electronic Notes in Theoretical Computer Science, 1622006, pp. 4960. 
 
[AD06b]  Amadio, R. and Dabrowski, F.  Feasible reactivity for synchronous cooperative threads  Electronic Notes in Theoretical Computer Science, 15432006. 
 
[BD06]  Boussinot, F. and Dabrowski, F.  Secure Multicore Programming  2006. 
 
[Bou06]  Boudol, G.  On strong normalization and type inference in the intersection type discipline  invited paper for a special issue of TCS in honor of Mario Coppo, Mariangiola Dezani and Simona Ronchi on the occasion of their 60th birthday, 2006. 
 
[Dam06b]  Damien Ciabrini,  Stack Filtering for Source Level Debugging  To appear in Software: Practice and Experience, 2006. 
 
[Bou06b]  Boussinot, F.  FairThreads: mixing cooperative and preemptive threads in C  Concurrency and Computation: Practice and Experience, 18(DOI: 10.1002/cppe.919), 2006, pp. 445469. 


 
[Bou06c]  Boudol, G.  Cooperative vs preemptive scheduling: a tradeoff, or: typing termination in a higherorder imperative language  draft, submitted, 2006. 
 
[DB06]  Dabrowski, F. and Boussinot, F.  Cooperative Threads and Preemptive Computations  Proceedings of TV'06, Multithreading in Hardware and Software: Formal Approaches to Design and Verification, Seattle, 2006. 
 [ http://www.easychair.org/FLoC06/TVpreproceedings.pdf ] 
 
[Bou06d]  Boudol, G.  Secure information flow as a safety property  unpublished draft, 2006. 
 
[Bou06e]  Boussinot, F.  FairThreads: mixing cooperative and preemptive threads in C  Concurrency and Computation: Practice and Experience, 18(DOI: 10.1002/cppe.919), 2006, pp. 445469. 


 
[Bou05]  Boussinot, F.  Cyclone+Loft  September, 2005. 
 [ ftp://ftpsop.inria.fr/pub/rapports/RR5680.ps.gz ] 
 
[DG05]  Dal Zilio, S. and Gascon, R.  Resource Bound Certification for a TailRecursive Virtual Machine  APLAS 2005  3rd Asian Symposium on Programming Languages and Systems, Lecture Notes in Computer Science, Nov, 2005, pp. 247263. 
 [ http://www.cmi.univmrs.fr/ dalzilio/Papers/sizeaplas2005.pdf ] 

 We define a method to statically bound the size of values computed during the execution of a program as a function of the size of its parameters. More precisely, we consider bytecode programs that should be executed on a simple stack machine with support for algebraic data types, patternmatching and tailrecursion. Our size verification method is expressed as a static analysis, performed at the level of the bytecode, that relies on machinecheckable certificates. We follow here the usual assumption that code and certificates may be forged and should be checked before execution. Our approach extends a system of static analyses based on the notion of quasiinterpretations that has already been used to enforce resource bounds on firstorder functional programs. This paper makes two additional contributions. First, we are able to check optimized programs, containing instructions for unconditional jumps and tailrecursive calls, and remove restrictions on the structure of the bytecode that was imposed in previous works. Second, we propose a direct algorithm that depends only on solving a set of arithmetical constraints. 

 
[ABD05]  Acciai, L. and Boreale, M. and Dal Zilio, S.  A Typed Calculus for Querying Distributed XML Documents  NWPT 2005  17th Nordic Workshop on Programming Theory, Oct, 2005. 

 We study the problems related to querying large, distributed XML documents. Our proposal takes the form of a new process calculus in which XML data are processes that can be queried by means of concurrent patternmatching expressions. What we achieve is a functional, stronglytyped programming model based on three main ingredients: an asynchronous process calculus in the style of Milner's picalculus and existing semantics for concurrentML; a model where documents and expressions are both represented as processes, and where evaluation is represented as a parallel composition of the two; a static type system based on regular expression types. 

 
[GS05]  Gallesio, E. and Serrano, M.  Ubiquitous Mail  Proceedings of the Sixth Acm sigplan Workshop on Scheme and Functional Programming, Tallinn, Estonia, Sep, 2005, pp. 6976. 
 [ html ] 

 Bimap is a tool for synchronizing IMAP servers. It enables two or more IMAP mirrored servers to be modified independently and later on, synchronized. Bimap is versatile so, in addition to synchronizing emails, it can be used for filtering and classifying emails. For the sake of the example, the paper shows automatic emails classification and whitelisting programmed with Bimap.
Bimap is implemented in Scheme. The most important parts of its implementation are presented in this paper with the intended goal to demonstrate that Scheme is suited for programming tasks that are usually devoted to scripting languages such as Perl or Python. With additional libraries, Scheme enables compact and efficient implementation of this distributed networked application because the main computations that require efficiency are executed in compiled code and only the user configurations are executed in interpreted code. 

 
[Loi05]  Loitsch, F.  Javascript Compilation  Proceedings of the Sixth Workshop on Scheme and Function Programming, Tallinn, Estonia, Sep, 2005, pp. 101111. 

 Jsigloo compiles Javascript to Scheme. It acts as an frontend to Bigloo which subsequently compiles the intermediate result to one of its backends (C, JVM or .NET). Such a compilation furthermore benefits of the optimizations implemented within Bigloo. Jsigloo hence implements only few optimizations, but tries to produce easily optimizable Scheme code. Scheme is (by design) a relatively minimal language, and some Javascript constructs don't have equivalent expressions in Scheme. This paper presents the difficulties we encountered when mapping these constructs. It furthermore describes the optimizations that have been implemented in Jsigloo. 

 
[ABB05]  Amadio, R. et al.  Reactive concurrent programming revisited  Bertinoro, Aug, 2005. 
 [ pdf ] 
 
[AD05]  Amadio, R. and Dabrowski, F.  Feasible Reactivity for Synchronous Cooperative Threads  12th workshop Expressiveness in Concurrency, Electronic Notes in Theoretical Computer Science, San Francisco, USA, Aug, 2005. 
 
[DG05b]  Dal Zilio, S. and Gascon, R.  Resource Bound Certification for a TailRecursive Virtual Machine  26, LIF, Jun, 2005. 
 
[BZ05]  Boudol, G. and Zimmer, P.  On type inference in the intersection type discipline  Electronic Notes in Theoretical Computer Science, 1362005, pp. 2342. 
 [ html ] 
 
[Ama05]  Amadio, R.  The SL synchronous language, revisited  Laboratoire PPS, Université de Paris 7, 2005. 
 
[Dam05]  Damien Ciabrini,  Stack virtualization for source level debugging  John Wiley & Sons, Ltd, 2005. 
 
[ABB05b]  Amadio, R. et al.  Reactive concurrent programming revisited  NS053, BRICS Notes Series, 2005, pp. 1220. 
 [ pdf ] 
 
[Bou05b]  Boudol, G.  On typing information flow  International Colloquium on Theoretical Aspects of Computing, Lecture Notes in Computer Science, 2005, pp. 366380. 
 [ html ] 
 
[DB05]  Dabrowsky, F. and Boussinot, F.  Cooperative Threads and Preemptive Computations  2005. 
 
[Bou05c]  Boudol, G.  A generic membrane model  Second Global Computing Workshop, Lecture Notes in Computer Science, 2005, pp. 209222. 
 [ html ] 
 
[AB05]  Almeida Matos, A. and Boudol, G.  On declassification and the nondisclosure policy  Computer Security Foundation Workshop, 2005, pp. 226240. 
 [ html ] 
 
[ABB05c]  Amadio, R. et al.  Reactive concurrent programming revisited  NS053, BRICS Notes Series, 2005, pp. 1220. 
 [ pdf ] 
 
[AB05b]  Almeida Matos, A. and Boudol, G.  On declassification and the nondisclosure policy  Computer Security Foundation Workshop, 2005, pp. 226240. 
 [ html ] 
 
[Alm05]  Almeida Matos, A.  Nondisclosure for distributed mobile code  FSTTCS'05, Lecture Notes in Computer Science, 2005. 
 
[ABC05]  Almeida Matos, A. and Boudol, G. and Castellani, I.  Typing Noninterference for Reactive Programs  5594, INRIA, 2005. 
 [ html ] 
 
[Ama05b]  Amadio, R.  Synthesis of maxplus quasiinterpretations  Fundamenta Informaticae, 652005, pp. 2960. 
 
[GS05b]  Gallesio, E. and Serrano, M.  Skribe: a Functional Authoring Language  Journal of Functional Programming, 2005. 
 [ html ] 

 Skribe is a functional programming language designed for authoring documents, such as web pages or technical reports. It is built on top of the Scheme programming language. Its concrete syntax is simple and it looks familiar to anyone used to markup languages. Authoring a document with Skribe is as simple as with HTML or LaTeX. Because of the conciseness of its original syntax, it is even possible to use it without noticing that it is a programming language. In Skribe, the ratio "markup/text" is smaller than with the other markup systems we have tested. 

 
[Bou04]  Boudol, G.  Safe recursive boxes  RR5115, INRIA, February, 2004. 
 [ html ] 
 
[Cia04]  Ciabrini, D.  Debugging Scheme Fair Threads  Proceedings of the 5th ACMSIGPLAN Workshop on Scheme and Functional Programming, Snowbird, UT, USA, September, 2004, pp. 7588. 
 [ http://wwwsop.inria.fr/mimosa/fp/Bugloo ] 
 
[Ama04]  Amadio, R.  Synthesis of maxplus quasiinterpretations  182004, LIF, Marseille, France, January, 2004. 
 
[Epa04]  Epardaud, S.  Mobile reactive programming in ULM  Proceedings of the Fifth ACM SIGPLAN Workshop on Scheme and Functional Programming, Snowbird, Utah, Sep 22,, 2004, pp. 8798. 
 [ http://wwwsop.inria.fr/mimosa/Stephane.Epardaud/papers/ulmscheme2004.pdf  pdf ] 

 We present the embedding of ULM in Scheme and an implementation of a compiler and virtual machine for it. ULM is a core programming model that allows multithreaded and distributed programming via strong mobility with a deterministic semantics. We present the multithreading and distributed primitives of ULM step by step using examples. The introduction of mobility in a Scheme language raises questions about the semantics of variables with respect to migration. We expose the problems and offer two solutions alongside ULM's network references. We also present our implementation of the compiler, virtual machine and the concurrent threading library written in Scheme. 

 
[BSS04]  Bres, Y. and Serpette, B. and Serrano, M.  Bigloo.NET: compiling Scheme to .NET CLR  Journal of Object Technology, 3(9), Oct, 2004. 
 [ html  issue_2004_09 ] 

 This paper presents the compilation of the Scheme programming language to .NET. This platform provides a virtual machine, the Common Language Runtime (CLR), that executes bytecode, the Common Intermediate Language (CIL). Since CIL was designed with language agnosticism in mind, it provides a rich set of language constructs and functionalities. As such, the CLR is the first execution environment that offers type safety, managed memory, tail recursion support and several flavors of pointers to functions. Therefore, the CLR presents an interesting ground for functional language implementations.
We discuss how to map Scheme constructs to CIL. We present performance analyses on a large set of reallife and standard Scheme benchmarks. In particular, we compare the speed of these programs when compiled to C, JVM and .NET. We show that in term of speed performance of the Mono implementation of .NET, the best implementing running on both Windows and Linux, still lags behind C and fast JVMs such as the Sun's implementations. 

 
[C. 04]  C. Brunette,  Construction et simulation graphiques de comportements: le modèle des Icobjs  Thèse de doctorat, Université de NiceSophia Antipolis, Oct, 2004. 
 
[Tar04]  Tardieu, O.  Loops in Esterel: from operational semantics to formally specified compilers  Ecole des Mines de Paris, Sep, 2004. 
 
[SBS04]  Serrano, M. and Boussinot, F. and Serpette, B.  Scheme Fair Threads  6th sigplan International Conference on Principles and Practice of Declarative Programming (PPDP), Verona, Italy, Aug, 2004, pp. 203214. 
 [ html ] 

 This paper presents Fair Threads, a new model for concurrent programming. This multithreading model combines preemptive and cooperative scheduling. User threads execute according to a cooperative strategy. Service threads execute according to a preemptive strategy. User threads may ask services from service threads in order to improve performance by exploiting hardware parallelism and in order to execute nonblocking operations.
Fair threads are experimented within the context of the functional programming language Scheme. This paper also presents the integration in this language. That is, it presents a semantics for Scheme augmented with Fair Threads and the main characteristics of the implementation. 

 
[Tar04b]  Tardieu, O.  A deterministic logical semantics for Esterel  Proceedings of the Workshop on Structural Operational Semantics, London, United Kingdom, Aug, 2004. 
 
[BSS04b]  Bres, Y. and Serpette, B. and Serrano, M.  Compiling Scheme programs to .NET Common Intermediate Language  2nd International Workshop on .NET Technologies, Plzen, Czech Republic, May, 2004. 
 [ pdf ] 

 We present in this paper the compilation of the Scheme programming language to .Net platform. .Net provides a virtual machine, the Common Language Runtime (CLR), that executes bytecode, the Common Intermediate Language (CIL). Since CIL was designed with language agnosticism in mind, it provides a rich set of language constructs and functionalities. Therefore, the CLR is the first execution environment that offers type safety, managed memory, tail recursion support and several flavors of pointers to functions. As such, the CLR presents an interesting ground for functional language implementations.
We discuss how to map Scheme constructs to CIL. We present performance analyses on a large set of reallife and standard Scheme benchmarks. In particular, we compare the performances of Scheme programs when compiled to C, JVM and .Net. We show that .Net still lags behind C and JVM. 

 
[Bou04b]  Boussinot, F.  Reactive Programming of Cellular Automata  RR5183, Inria, May, 2004. 
 
[Tar04c]  Tardieu, O.  Goto and Concurrency: Introducing Safe Jumps in Esterel  Proceedings of the Workshop on Synchronous Languages, Applications, and Programming, Barcelona, Spain, Mar, 2004. 
 
[DL04]  Dal Zilio, S. and Lugiez, D.  A Logic you Can Count On  POPL 2004  31st Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Jan, 2004. 

 We prove the decidability of the quantifierfree, static fragment of ambient logic, with composition adjunct and iteration, which corresponds to a kind of regular expression language for semistructured data. The essence of this result is a surprising connection between formulas of the ambient logic and counting constraints on (nested) vectors of integers. Our proof method is based on a new class of tree automata for unranked, unordered trees, which may result in practical algorithms for deciding the satisfiability of a formula. A benefit of our approach is to naturally lead to an extension of the logic with recursive definitions, which is also decidable. Finally, we identify a simple syntactic restriction on formulas that improves the effectiveness of our algorithms on large examples. 

 
[MBC04]  Matos, A. and Boudol, G. and Castellani, I.  Typing noninterference for reactive programs  Foundations of Computer Security, 2004. 
 [ pdf ] 
 
[Dab04]  Dabrowski, F.  Reactivity in ULM  2004. 
 
[BZ04]  Boudol, G. and Zimmer, P.  On type inference in the intersection type discipline  ITRS'04 Workshop, 2004. 
 [ html ] 
 
[Van04]  Vanackere, V.  HistoryDependent Scheduling for Cryptographic Processes  Proc. VMCAI' 2004, Lecture Notes in Computer Science, Venice, Italy, 2004. 
 
[Bou04c]  Boudol, G.  A generic membrane model  Second Global Computing Workshop, 2004. 
 [ html ] 
 
[Bou04d]  Boussinot, F.  Concurrent Programming with Fair Threads  The LOFT Language  2004. 
 [ html  pdf ] 
 
[Zim04]  Zimmer, P.  Récursion généralisée et inférence de types avec intersection  Thèse de doctorat, Université de Nice Sophia Antipolis, France. INRIA Sophia Antipolis, 2004. 
 [ ps ] 
 
[Bou04e]  Boudol, G.  The Recursive Record Semantics of Objects Revisited  Journal of Functional Programming, 142004, pp. 263315. 
 [ html ] 
 
[AD04]  Amadio, R. M. and Dal Zilio, S.  Resource Control for Synchronous Cooperative Threads  CONCUR 2004  15th International Conference on Concurrency Theory, Lecture Notes in Computer Science, 2004, pp. 6882. 

 We develop new methods to statically bound the resources needed for the execution of systems of concurrent, interactive threads. Our study is concerned with a synchronous model of interaction based on cooperative threads whose execution proceeds in synchronous rounds called instants. Our contribution is a system of compositional static analyses to guarantee that each instant terminates and to bound the size of the values computed by the system as a function of the size of its parameters at the beginning of the instant. Our method generalises an approach designed for firstorder functional languages that relies on a combination of standard termination techniques for term rewriting systems and an analysis of the size of the computed values based on the notion of quasiinterpretation. These two methods can be combined to obtain an explicit polynomial bound on the resources needed for the execution of the system during an instant. 

 
[Dab04b]  Dabrowski, F.  Side effects and polynomial bounds  2004. 
 
[Bou04f]  Boudol, G.  ULM, a core programming model for global computing  ESOP'04, Lecture Notes in Computer Science, 2004, pp. 234248. 
 [ html ] 
 
[ACD04]  Amadio, R. M. et al.  A Functional Scenario for Bytecode Verification of Resource Bounds  CSL 2004  18th International Conference on Computer Science Logic, Lecture Notes in Computer Science, 2004, pp. 265279. 

 We define a simple stack machine for a firstorder functional language and show how to perform type, size, and termination verifications at the level of the bytecode of the machine. In particular, we show that a combination of size verification based on quasiinterpretations and of termination verification based on lexicographic path orders leads to an explicit bound on the space required for the execution. 

 
[TZH04]  Teller, D. and Zimmer, P. and Hirschkoff, D.  Using ambients to control resources  International Journal of Information Security, 22004, pp. 126144. 
 [ pdf ] 
 
[ACD04b]  Amadio, R. M. et al.  A Functional Scenario for Bytecode Verification of Resource Bounds  CSL 2004  18th International Conference on Computer Science Logic, Lecture Notes in Computer Science, 2004, pp. 265279. 

 We define a simple stack machine for a firstorder functional language and show how to perform type, size, and termination verifications at the level of the bytecode of the machine. In particular, we show that a combination of size verification based on quasiinterpretations and of termination verification based on lexicographic path orders leads to an explicit bound on the space required for the execution. 

 
[CDG03]  Charatonik, W. et al.  Model Checking Mobile Ambients  Theoretical Computer Science, 308(1), Nov, 2003, pp. 277331. 

 We settle the complexity bounds of the model checking problem for the ambient calculus with public names against the ambient logic. We show that if either the calculus contains replication or the logic contains the guarantee operator, the problem is undecidable. In the case of the replicationfree calculus and guaranteefree logic we prove that the problem is PSPACEcomplete. For the complexity upper bound, we devise a new representation of processes that remains of polynomial size during process execution; this allows us to keep the model checking procedure in polynomial space. Moreover, we prove PSPACEhardness of the problem for several quite simple fragments of the calculus and the logic; this suggests that there are no interesting fragments with polynomialtime model checking algorithms. 

 
[Aco03]  AcostaBermejo, R.  Rejo  Langage d'objets réactifs et d'agents  Thèse de doctorat de l'ENSMP, Oct, 2003. 
 [ ftp://ftpsop.inria.fr/mimosa/rp/bibliography/TheseRaulACOSTA.pdf ] 
 
[CS03]  Ciabrini, D. and Serrano, M.  Bugloo: A Source Level Debugger for Scheme Programs Compiled into JVM Bytecode  3th International Lisp Conference, New York, USA, Oct, 2003. 
 [ http://wwwsop.inria.fr/mimosa/fp/Bugloo ] 
 
[GS03]  Gallesio, E. and Serrano, M.  Programming Graphical User Interfaces with Scheme  Journal of Functional Programming, 13(5), Sep, 2003, pp. 839886. 
 [ ps.gz ] 

 This paper presents Biglook, a widget library for an extended version of the Scheme programming language. It uses classes of a Closlike object layer to represent widgets and Scheme closures to handle graphical events. Combining functional and objectoriented programming styles yields an original application programming interface that advocates a strict separation between the implementation of the graphical interfaces and the userassociated commands, enabling compact source code.
The Biglook implementation separates the Scheme programming interface and the native backend. This permits different ports for Biglook. The current version uses GTK and Swing graphical toolkits, while the previous release used Tk. 

 
[DL03]  Dal Zilio, S. and Lugiez, D.  XML Schema, Tree Logic and Sheaves Automata  RTA 2003  14th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science, Jun, 2003, pp. 246263. 
 [ http://www.cmi.univmrs.fr/ dalzilio/Papers/sheavesxml.pdf ] 

 XML documents, and other forms of semistructured data, may be roughly described as edge labeled trees; it is therefore natural to use tree automata to reason on them. This idea has already been successfully applied in the context of Document Type Definition (DTD), the simplest standard for defining XML documents validity, but additional work is needed to take into account XML Schema, a more advanced standard, for which regular tree automata are not satisfactory. In this paper, we define a tree logic that directly embeds XML Schema as a plain subset as well as a new class of automata for unranked trees, used to decide this logic, which is wellsuited to the processing of XML documents and schemas. 

 
[Ser03]  Serrano, M.  Langage C++, ch. Techniques de l'ingénieur, 249, rue de Crimée, 75925 Paris, Cedex 19, France, 2003. 
 [ http://www.techniquesingenieur.fr ] 
 
[TZH03]  Teller, D. and Zimmer, P. and Hirschkoff, D.  Using ambients to control resources  Schedae Informaticae, 122003, pp. 113127. 
 
[Gua03]  Guan, X.  Towards a tree of channels  Electronic Notes in Theoretical Computer Science, 2003. 
 
[Bou03]  Boudol, G.  On strong normalization in the intersection type discipline  TLCA'03, Lecture Notes in Computer Science, 2003, pp. 6074. 
 [ html ] 
 
[Zim03]  Zimmer, P.  On the expressiveness of pure safe ambients  Mathematical Structures in Computer Science, 132003, pp. 721770. 
 [ http://wwwsop.inria.fr/mimosa/personnel/Pascal.Zimmer/papers/mscs_pure_ambients.ps ] 
 
[Zim03b]  Zimmer, P.  On the expressiveness of pure mobile ambients  Electronic Notes in Theoretical Computer Science, 2003. 
 [ http://wwwsop.inria.fr/mimosa/personnel/Pascal.Zimmer/papers/express00.ps ] 
 
[ABL03]  Amadio, R. and Boudol, G. and Lhoussaine, C.  The receptive distributed picalculus  TOPLAS, 25(5), 2003, pp. 549577. 
 [ html ] 
 
[DF03]  Dal Zilio, S. and Formenti, E.  On the Dynamics of PB Systems: A Petri Net View  WMC 2003  Workshop on Membrane Computing, Lecture Notes in Computer Science, 2003, pp. 153167. 
 [ http://www.cmi.univmrs.fr/ dalzilio/Papers/finalpbs.pdf ] 

 We study dynamical properties of PB systems, a new computational model of biological processes, and propose a compositional encoding of PB systems into Petri nets. Building on this relation, we show that three properties: boundedness, reachability and cyclicity, which we claim are useful in practice, are all decidable. 

 
[DL02]  Dal Zilio, S. and Lugiez, D.  XML Schema, Tree Logic and Sheaves Automata  4631, INRIA, Nov, 2002. 
 [ http://www.cmi.univmrs.fr/ dalzilio/Papers/RR4631.pdf ] 

 We describe a new class of tree automata, and a related logic on trees, with applications to the processing of XML documents and XML schemas. XML documents, and other forms of semistructured data, may be roughly described as edge labeled trees. Therefore it is natural to use tree automata to reason on them and try to apply the classical connection between automata, logic and query languages. This approach has been followed by various researchers and has given some notable results, especially when dealing with Document Type Definition (DTD), the simplest standard for defining XML documents validity. But additional work is needed to take into account XML schema, a more advanced standard, for which regular tree automata are not satisfactory. A major reason for this inadequacy is the presence of an associativecommutative operator in the schema language, inherited from the &operator of SGML, and the inherent limitations of regular tree automata in dealing with associativecommutative algebras. The class of automata considered here, called sheaves automata, is a tailored version of automata for unranked trees with both associative and associativecommutative symbols already proposed by the authors. In order to handle both ordered and unordered operators, we combine the transition relation of regular tree automaton with regular word expression and counting constraints. This extension appears quite natural since, when no counting constraints occurs, we obtain hedge automata, a simple model for XML schemata, and when no constraints occur, we obtain regular tree automata. Building on the classical connection between logic and automata, we also present a decidable tree logic that embeds XML Schema as a plain subset. 

 
[SBS02]  Serrano, M. and Boussinot, F. and Serpette, B.  Scheme FairThreads  2th International Lisp Conference (invited paper), San Francisco, CA, USA, Oct, 2002. 
 
[SS02]  Serpette, B. and Serrano, M.  Compiling Scheme to JVM bytecode: a performance study  7th sigplan International Conference on Functional Programming (ICFP), Pittsburgh, Pensylvanie, USA, Oct, 2002. 
 [ ps.gz ] 

 We have added a Java virtual machine (henceforth JVM) bytecode generator to the optimizing SchemetoC compiler Bigloo. We named this new compiler BiglooJVM. We have used this new compiler to evaluate how suitable the JVM bytecode is as a target for compiling strict functional languages such as Scheme. In this paper, we focus on the performance issue. We have measured the execution time of many Scheme programs when compiled to C and when compiled to JVM. We found that for each benchmark, at least one of our hardware platforms ran the BiglooJVM version in less than twice the time taken by the Bigloo version. In order to deliver fast programs the generated JVM bytecode must be carefully crafted in order to benefit from the speedup of justintime compilers. 

 
[GS02]  Gallesio, E. and Serrano, M.  Biglook: a Widget Library for the Scheme Programming Language  2002 Usenix annual technical conference, Freenix track, Monterey, Californie, USA, Jun, 2002, pp. 8597. 
 [ ps.gz ] 
 
[SG02]  Serrano, M. and Gallesio, E.  This is Scribe!  3th Acm sigplan Workshop on Scheme and Functional Programming, Pittsburgh, Pennsylvania, USA, Jun, 2002. 
 [ ps.gz  html ] 

 This paper presents Scribe, a functional programming language for authoring documents. Even if it is a general purpose tool, it best suits the writing of technical documents such as web pages or technical reports, API documentations, etc. Executing Scribe programs can produce documents of various formats such as PostScript, PDF, HTML, Texinfo or Unix man pages. That is, the very same program can be used to produce documents in different formats. Scribe is a full featured programming language but it looks like a markup language à la HTML. 

 
[DL02b]  Dal Zilio, S. and Lugiez, D.  Multitrees Automata, Presburger's Constraints and Tree Logics  082002, LIF, Jun, 2002. 
 [ http://www.cmi.univmrs.fr/ dalzilio/Papers/rrlif082002.ps ] 

 We describe multitree automata and a related logic on multitrees. Multitrees are extensions of trees with both associative and associativecommutative symbols that may bear arbitrary numbers of sons. An originality of our approach is that transitions of an automaton are restricted using Presburger's constraints. The benefit of this extension is that we generalize, all together, automata with equality and disequalities constraints as well as counting constraints. This new class of automata appears very general as it may encompass hedge automata, a simple yet effective model for XML schemata, feature tree automata, automata with constraints between brothers and automata with arithmetical constraints. Moreover, the class of recognizable languages enjoys all the typical good properties of traditional regular languages: closure under boolean operations and composition by associative and associativecommutative operators, determinisation, decidability of the test for emptiness, ... We apply our automata to query languages for XMLlike documents and to automated inductive theorem proving based on rewriting, obtaining each time new results. Using a classical connection between logic and automata, we design a decidable logic for (multi)trees that can be used as a foundation for querying XMLlike document. This proposition has the same flavour as a query language for semistructured recently proposed by Cardelli and Ghelli. The same tree logic is used to yield decidable cases of inductive reducibility modulo associativitycommutativity, a key property in inductive theorem proving based on rewriting. 

 
[DG02]  Dal Zilio, S. and Gordon, A.  Region analysis and a picalculus with groups  Journal of Functional Programming, 12(3), May, 2002, pp. 229292. 

 We show that the typed region calculus of Tofte and Talpin can be encoded in a typed picalculus equipped with name groups and a novel effect analysis. In the region calculus, each boxed value has a statically determined region in which it is stored. Regions are allocated and deallocated according to a stack discipline, thus improving memory management. The idea of name groups arose in the typed ambient calculus of Cardelli, Ghelli, and Gordon. There, and in our picalculus, each name has a statically determined group to which it belongs. Groups allow for typechecking of certain mobility properties, as well as effect analyses. Our encoding makes precise the intuitive correspondence between regions and groups. We propose a new formulation of the type preservation property of the region calculus, which avoids Tofte and Talpin's rather elaborate coinductive formulation. We prove the encoding preserves the static and dynamic semantics of the region calculus. Our proof of the correctness of region deallocation shows it to be a specific instance of a general garbage collection principle for the picalculus with effects. We propose new equational laws for letregion, analogous to scope mobility laws in the picalculus, and show them sound in our semantics. 

 
[TZH02]  Teller, D. and Zimmer, P. and Hirschkoff, D.  Using ambients to control resources  Proceedings of CONCUR 2002, LNCS, 2002, pp. 288303. 
 [ http://wwwsop.inria.fr/mimosa/personnel/Pascal.Zimmer/papers/concur02.ps ] 
 
[Zim02]  Zimmer, P.  On the expressiveness of pure safe ambients  INRIA Research Report RR4350, 2002. 
 [ http://wwwsop.inria.fr/mimosa/personnel/Pascal.Zimmer/papers/RR4350.ps ] 
 
[BZ02]  Boudol, G. and Zimmer, P.  Recursion in the callbyvalue lambdacalculus  Proceedings of FICS 2002 (Fixed Points in Computer Science), BRICS Notes Series NS022, 2002. 
 [ http://wwwsop.inria.fr/mimosa/personnel/Pascal.Zimmer/papers/fics02.ps ] 
 
[ABL02]  Amadio, R. and Boudol, G. and Lhoussaine, C.  On message deliverability and nonuniform receptivity  Fundamenta Informaticae, 53(2), 2002, pp. 105130. 
 [ html ] 
 
[TZH02b]  Teller, D. and Zimmer, P. and Hirschkoff, D.  Using ambients to control resources  LIP Research Report N. 200216, ENS Lyon, 2002. 
 [ http://wwwsop.inria.fr/mimosa/personnel/Pascal.Zimmer/papers/RR200216.ps ] 
 
[BC02]  Boudol, G. and Castellani, I.  Noninterference for concurrent programs and thread systems  Theoretical Computer Science, 281(1), 2002, pp. 109130. 
 [ html ] 
 
[BC02b]  Boudol, G. and Castellani, I.  Noninterference for Concurrent Programs and Thread Systems  Theoretical Computer Science, 281(1), 2002, pp. 109130. 
 
[Dal01]  Dal Zilio, S.  Fixed Points in the Ambient Logic  FICS 2001  3rd Workshop on Fixed Points in Computer Science, Sep, 2001. 
 [ http://www.cmi.univmrs.fr/ dalzilio/Papers/puzzle.pdf ] 

 We present an extension of the ambient logic with fixed points operators in the style of the µcalculus. We give a simple syntactic condition for the equivalence between minimal and maximal fixpoint formulas and show how to subsume spatial analogues of the usual box and diamond operators. 

 
[Dal01b]  Dal Zilio, S.  Mobile Processes: a Commented Bibliography  MOVEP '2k  4th Summer school on Modelling and Verification of Parallel processes, Lecture Notes in Computer Science, Jun, 2001, pp. 206222. 
 [ http://www.cmi.univmrs.fr/ dalzilio/Papers/survey.pdf ] 

 We propose a short bibliographic survey of calculi for mobile processes. Contrasting with other similar exercises, we consider two related, but distinct, notions of mobile processes, namely labile processes, which can exhibit changes of their interaction structure, as modelled in the picalculus, and motile processes, which can exhibit movement, as modelled in the ambient calculus of Cardelli and Gordon. A common attribute of the algebraic frameworks presented in this paper is that they all rely on a notion of name as first class value. 

 
[CDG01]  Charatonik, W. et al.  The Complexity of Model Checking Mobile Ambients  MSRTR200103, Microsoft Research, May, 2001. 
 [ http://www.cmi.univmrs.fr/ dalzilio/Papers/tr200103.ps ] 

 We settle the complexity bounds of the model checking problem for the replicationfree ambient calculus with public names against the ambient logic without parallel adjunct. We show that the problem is PSPACEcomplete. For the complexity upperbound, we devise a new representation of processes that remains of polynomial size during process execution; this allows us to keep the model checking procedure in polynomial space. Moreover, we prove PSPACEhardness of the problem for several quite simple fragments of the calculus and the logic; this suggests that there are no interesting fragments with polynomialtime model checking algorithms. 

 
[CDG01b]  Charatonik, W. et al.  The Complexity of Model Checking Mobile Ambients  FoSSaCS 2001  4th International Conference on Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, Apr, 2001, pp. 152167. 
 [ http://www.cmi.univmrs.fr/ dalzilio/Papers/fossacs2001.pdf ] 

 We settle the complexity bounds of the model checking problem for the replicationfree ambient calculus with public names against the ambient logic without parallel adjunct. We show that the problem is PSPACEcomplete. For the complexity upperbound, we devise a new representation of processes that remains of polynomial size during process execution; this allows us to keep the model checking procedure in polynomial space. Moreover, we prove PSPACEhardness of the problem for several quite simple fragments of the calculus and the logic; this suggests that there are no interesting fragments with polynomialtime model checking algorithms. 

 
[BC01]  Boudol, G. and Castellani, I.  Noninterference for Concurrent Programs  ICALP'01, Lecture Notes in Computer Science, (2076), 2001, pp. 382395. 
 
[Cas01]  Castellani, I.  Process Algebras with Localities  NorthHolland, Amsterdam, 2001, pp. 9451045. 
 
[I. 01]  I. Castellani,  Process Algebras with Localities  NorthHolland, Amsterdam, 2001, pp. 9451045. 
 
[BSD01]  Boussinot, F. et al.  A reactive behavior framework for dynamic virtual worlds  Web3D, 2001, pp. 6975. 
 
[SB00]  Serrano, M. and Boehm, H.  Understanding Memory Allocation of Scheme Programs  5th sigplan International Conference on Functional Programming (ICFP), Montréal, Québec, Canada, Sep, 2000, pp. 245256. 
 [ ps.gz ] 

 Memory is the performance bottleneck of modern architectures. Keeping memory consumption as low as possible enables fast and unobtrusive applications. But it is not easy to estimate the memory use of programs implemented in functional languages, due to both the complex translations of some high level constructs, and the use of automatic memory managers.
To help understand memory allocation behavior of Scheme programs, we have designed two complementary tools. The first one reports on frequency of allocation, heap configurations and on memory reclamation. The second tracks down memory leaks. We have applied these tools to our Scheme compiler, the largest Scheme program we have been developing. This has allowed us to drastically reduce the amount of memory consumed during its bootstrap process, without requiring much development time.
Development tools will be neglected unless they are both conveniently accessible and easy to use. In order to avoid this pitfall, we have carefully designed the user interface of these two tools. Their integration into a real programming environment for Scheme is detailed in the paper. 

 
[Ser00]  Serrano, M.  Vers une programmation fonctionnelle praticable  Habilitation à diriger des recherches, Université de Nice SophiaAntipolis, Route des Colles, B.P. 145  F06903 SophiaAntipolis, CEDEX, Sep, 2000. 
 [ ps.gz ] 

 La production de logiciels informatiques ne se résume pas à la réalisation de « gros » programmes nécessitant des années d'effort fournies par des équipes imposantes. Bien souvent, on a besoin de petits programmes, dont la durée de vie est assez courte et qui sont écrits par une ou deux personnes. La course incessante à l'innovation des entreprises informatiques les contraint fréquemment à renoncer aux techniques de génie logiciel pour opter pour des techniques légères favorisant un développement court et souple.
Pour favoriser ce type de réalisations nous avons conçu un environnement de programmation qui repose sur un langage particulièrement concis et sur quelques outils permettant un développement rapide d'applications réalistes (un compilateur optimisant, des outils de mise au point, de navigation, etc.).
Le choix du langage de programmation pour un tel projet est primordial car c'est le langage qui façonne le système. Au risque de paraître hérétique, nous avons choisi Scheme, un langage fonctionnel, parce que cette famille de langages permet une écriture d'une concision presque sans égal.
Scheme est un petit langage. C'est parfois un atout (par exemple pour l'enseignement) mais c'est aussi souvent un handicap. Nous avons donc dû lui adjoindre de nombreuses extensions. Nous en présenterons deux au cours de cette soutenance: un langage de module et une couche objet. Nous nous efforcerons de montrer les liens reliant ces deux constructions et nous montrerons l'exploitation que nous avons faite de certaines caractéristiques de Scheme (comme, par exemple, le typage dynamique) pour augmenter encore l'expressivité de ce langage.
Scheme est connu pour être difficile à implanter (parce que sa concision repose sur un haut niveau d'abstraction sémantique): c'est pourquoi nous avons consacré une grande partie de nos recherches à la compilation de ce langage. Nous présentons quelques uns de ces travaux dans le mémoire. Notre compilateur Scheme occupe une place privilégiée dans notre environnement car c'est lui qui permet la production d'applications efficaces. Toutefois, il arrive que les programmes doivent être travaillés afin que leur performances soient améliorées. Sur les architectures récentes c'est souvent une mauvaise utilisation de la mémoire (allocation, récupération) qui est la cause de performances moyennes. Lorsque le compilateur seul ne parvient pas à optimiser les programmes sources, les utilisateurs de notre environnement peuvent avoir recours à deux outils permettant l'étude de la gestion de la mémoire dans leurs applications. 

 
[DG00]  Dal Zilio, S. and Gordon, A.  Region analysis and a \picalculus with groups  MFCS 2000  25th International Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, Aug, 2000, pp. 120. 
 [ http://www.cmi.univmrs.fr/ dalzilio/Papers/regionsmfcs.ps ] 

 We show that the typed region calculus of Tofte and Talpin can be encoded in a typed \picalculus equipped with name groups and a novel effect analysis. In the region calculus, each boxed value has a statically determined region in which it is stored. Regions are allocated and deallocated according to a stack discipline, thus improving memory management. The idea of name groups arose in the typed ambient calculus of Cardelli, Ghelli, and Gordon. There, and in our \picalculus, each name has a statically determined group to which it belongs. Groups allow for typechecking of certain mobility properties, as well as effect analyses. Our encoding makes precise the intuitive correspondence between regions and groups. We propose a new formulation of the type preservation property of the region calculus, which avoids Tofte and Talpin's rather elaborate coinductive formulation. We prove the encoding preserves the static and dynamic semantics of the region calculus. Our proof of the correctness of region deallocation shows it to be a specific instance of a general garbage collection principle for the \picalculus with effects. We propose new equational laws for \kwletregion, analogous to scope mobility laws in the \picalculus, and show them sound in our semantics. 

 
[DG00b]  Dal Zilio, S. and Gordon, A.  Region analysis and a \picalculus with groups  MSRTR200057, Microsoft Research, Aug, 2000. 
 [ http://www.cmi.univmrs.fr/ dalzilio/Papers/tr200057.ps ] 

 We show that the typed region calculus of Tofte and Talpin can be encoded in a typed picalculus equipped with name groups and a novel effect analysis. In the region calculus, each boxed value has a statically determined region in which it is stored. Regions are allocated and deallocated according to a stack discipline, thus improving memory management. The idea of name groups arose in the typed ambient calculus of Cardelli, Ghelli, and Gordon. There, and in our picalculus, each name has a statically determined group to which it belongs. Groups allow for typechecking of certain mobility properties, as well as effect analyses. Our encoding makes precise the intuitive correspondence between regions and groups. We propose a new formulation of the type preservation property of the region calculus, which avoids Tofte and Talpin's rather elaborate coinductive formulation. We prove the encoding preserves the static and dynamic semantics of the region calculus. Our proof of the correctness of region deallocation shows it to be a specific instance of a general garbage collection principle for the picalculus with effects. 

 
[Dal00]  Dal Zilio, S.  An Interpretation of Typed Concurrent Objects in the Blue Calculus  IFIP TCS 2000  International Conference on Theoretical Computer Science, Lecture Notes in Computer Science, Aug, 2000, pp. 409424. 
 [ http://www.cmi.univmrs.fr/ dalzilio/Papers/ifiptcs2000.pdf ] 

 We propose an interpretation of a typed concurrent calculus of objects based on the model of Abadi and Cardelli imperative object calculus. The target of our interpretation is a version of the blue calculus, a variant of the picalculus that directly contains the lambda calculus, with record and firstorder types. We show that reduction and type judgments can be derived in a rather simple and natural way, and that our encoding can be extended to selftypes and synchronization primitives. We also prove some equational laws on objects. 

 
[Dal00b]  Dal Zilio, S.  Spatial Congruence for the Ambients is Decidable  MSRTR200041, Microsoft Research, May, 2000. 
 [ http://www.cmi.univmrs.fr/ dalzilio/Papers/tr200041.pdf ] 

 The ambient calculus of Cardelli and Gordon is a process calculus for describing mobile computation where processes may reside within a hierarchy of locations, called ambients. The dynamic semantics of this calculus is presented in a chemical style that allows for a compact and simple formulation. In this semantics, an equivalence relation, the spatial congruence, is defined on the top of an unlabelled transition system, the reduction system. Reduction is used to represent a real step of evolution (in time), while spatial congruence is used to identify processes up to particular (spatial) rearrangements. In this paper, we show that it is decidable to check whether two ambient calculus processes are spatially congruent, or not. Our proof is based on a natural and intuitive interpretation of ambient processes as edgelabelled finitedepth trees. This allows us to concentrate on the subtle interaction between two key operators of the ambient calculus, namely restriction, that accounts for the dynamic generation of new location names, and replication, used to encode recursion. The result of our study is the definition of an algorithm to decide spatial congruence and a definition of a normal form for processes that is useful in the proof of interesting equivalence laws. 

 
[Ser00b]  Serrano, M.  Bee: an Integrated Development Environment for the Scheme Programming Language  Journal of Functional Programming, 10(2), May, 2000, pp. 143. 
 
[Ser00c]  Serrano, M.  Bee: an Integrated Development Environment for the Scheme Programming Language  Journal of Functional Programming, 10(2), May, 2000, pp. 143. 
 [ ps.gz ] 

 The Bee is an integrated development environment for the Scheme programming language. It provides the user with a connection between Scheme and the C programming language, a symbolic debugger, a profiler, an interpreter, an optimizing compiler that delivers stand alone executables, a source file browser, a project manager, user libraries and online documentation. This article details the facilities of the Bee, its user interface and presents an overview of the implementation of its main components. 

 
[BL00]  Boudol, G. and Laneve, C.  \lambdaCalculus, Multiplicites and the \piCalculus  Proof, Language and Interaction: Essays in Honour of Robin Milner, Foundations of Computing, May, 2000. 
 [ html ] 
 
[BS00]  Boussinot, F. and Susini, J.  Java Threads and SugarCubes  Software Practice and Experience, 30(14), 2000, pp. 545566. 
 
[Bou00b]  Boussinot, F.  Objets réactifs en Java  Collection Scientifique et Technique des Telecommunications, PPUR, 2000. 
 
[Zim00]  Zimmer, P.  Subtyping and Typing Algorithms for Mobile Ambients  Proceedings of FOSSACS'00, LNCS, 2000, pp. 375390. 
 [ http://wwwsop.inria.fr/mimosa/personnel/Pascal.Zimmer/papers/fossacs00.ps ] 
 
[Bou00c]  Boussinot, F.  Objets réactifs en Java  Presses Polytechniques Universitaires Romandes, 2000. 
 
[Zim00b]  Zimmer, P.  On the expressiveness of pure mobile mmbients  Proceedings of EXPRESS'00 (Expressiveness in Concurrency), BRICS Notes Series NS002, 2000. 
 [ http://wwwsop.inria.fr/mimosa/personnel/Pascal.Zimmer/papers/express00.ps ] 
 
