Mimosa

Classified publications

Here is our classified list of publications:

Chronological bibliography

2010

2009

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.

2008

[BD08]	Boussinot, F. and Dabrowski, F. -- Safe Reactive Programming: the FunLoft Proposal -- Proc. of MULTIPROG -- First Workshop on Programmability Issues for Multi-Core 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. 116-130.

[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 Client-Side Compilation -- Moraz M. T. editor, Seton Hall University, Intellect Bristol, UK/Chicago, USA, 2008, pp. 141--158.

[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. 63-81.

2007

[Cas07] Castellani, I. -- State-oriented 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 full-fledged Web server for executing the server-side 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 pi-calculus -- Proceedings ACM SIGPLAN Principles and Practice of Declarative Programming , Jul, 2007, pp. 45-55 .

[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 Client-Side 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 server-side scripting languages (such as PHP, JSP, ...) with a unique language that unites client-side interactions and server-side 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 client-side 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 tail-recursive 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 hand-written 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 Client-Side 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 Computer-Aided Design of Integrated Circuits and Systems, 26(3), Mar, 2007, pp. 456--467.

[TE07] Tardieu, O. and Edwards, S. -- Instantaneous Transitions in Esterel -- Proceedings of the Workshop on Model-Driven High-Level 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. 121-150 .

[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/inria-00174843, Inria, 2007.

[BD07] Boussinot, F. and Dabrowski, F. -- Formalisation of FunLoft. http://hal.inria.fr/inria-00183242 -- 2007.

[Ama07b] Amadio, R. -- A synchronous pi-calculus -- Information and Computation. 205(9):1470-1490, 2007.

[Bou07c] Boudol, G. -- Fair cooperative multithreading, or: typing termination in a higher-order concurrent imperative language -- CONCUR'07, Lecture Notes in Computer Science, 2007, pp. 272-286.

[BD07b] Boussinot, F. and Dabrowsky F., -- Formalisation of FunLoft -- http://hal.inria.fr/inria-00183242, 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. 124-156.

[Bou07d] Boussinot, F. -- A Benchmark for Multicore Machines. http://hal.inria.fr/inria-00174843 -- 2007.

[BK07] Boudol, G. and Kolundzija, M. -- Access control and declassification -- MMM-ACNS'07, Communications in Computer and Information Science, 2007.

[Cas07b] Castellani, I. -- State-oriented noninterference for CCS -- ENTCS, 2007, pp. 39-60.

[ ]

2006

[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. -- Scheduling-independent threads and exceptions in SHIM -- Proceedings of the 6th ACM IEEE International conference on Embedded software, Seoul, Korea, Oct, 2006, pp. 142--151.

[Dam06]

Damien Ciabrini, -- Débogage symbolique multi-langages pour les plates-formes d'exécution généralistes -- Université de Nice Sophia Antipolis, Oct, 2006.

[ php?label=INRIA&action_todo=view&langue=en&id=tel-00122789&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 higher-order 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 HTML-based 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 pi-calculus, Draft -- 2006.

[Van06]

Van Bakel, S. -- The heart of intersection type assignment -- RR-5984, INRIA, 2006.

[Ama06]

Amadio, R. -- A synchronous pi-calculus -- Université Paris 7, Laboratoire PPS, 2006.

[AD06]

Amadio, R. and Dal Zilio, S. -- Resource control for synchronous cooperative threads -- Theoretical Computer Science, 3582006, pp. 229-254.

[ABB06]

Amadio, R. et al. -- Reactive concurrent programming revisited -- Electronic Notes in Theoretical Computer Science, 1622006, pp. 49-60.

[AD06b]

Amadio, R. and Dabrowski, F. -- Feasible reactivity for synchronous cooperative threads -- Electronic Notes in Theoretical Computer Science, 154-32006.

[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. 445-469.

Fair threads in C.

[Bou06c]

Boudol, G. -- Cooperative vs preemptive scheduling: a trade-off, or: typing termination in a higher-order 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/FLoC-06/TV-preproceedings.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. 445-469.

Fair threads in C.

2005

[Bou05]

Boussinot, F. -- Cyclone+Loft -- September, 2005.

[ ftp://ftp-sop.inria.fr/pub/rapports/RR-5680.ps.gz ]

[DG05]

Dal Zilio, S. and Gascon, R. -- Resource Bound Certification for a Tail-Recursive Virtual Machine -- APLAS 2005 -- 3rd Asian Symposium on Programming Languages and Systems, Lecture Notes in Computer Science, Nov, 2005, pp. 247--263.

[ http://www.cmi.univ-mrs.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, pattern-matching and tail-recursion. Our size verification method is expressed as a static analysis, performed at the level of the bytecode, that relies on machine-checkable 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 quasi-interpretations that has already been used to enforce resource bounds on first-order functional programs. This paper makes two additional contributions. First, we are able to check optimized programs, containing instructions for unconditional jumps and tail-recursive 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 pattern-matching expressions. What we achieve is a functional, strongly-typed programming model based on three main ingredients: an asynchronous process calculus in the style of Milner's pi-calculus and existing semantics for concurrent-ML; 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. 69--76.

[ 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 white-listing 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. 101-111.

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 Tail-Recursive 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. 23-42.

[ 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 -- NS-05-3, BRICS Notes Series, 2005, pp. 12-20.

[ pdf ]

[Bou05b]

Boudol, G. -- On typing information flow -- International Colloquium on Theoretical Aspects of Computing, Lecture Notes in Computer Science, 2005, pp. 366-380.

[ 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. 209-222.

[ html ]

[AB05]

Almeida Matos, A. and Boudol, G. -- On declassification and the non-disclosure policy -- Computer Security Foundation Workshop, 2005, pp. 226-240.

[ html ]

[ABB05c]

Amadio, R. et al. -- Reactive concurrent programming revisited -- NS-05-3, BRICS Notes Series, 2005, pp. 12-20.

[ pdf ]

[AB05b]

Almeida Matos, A. and Boudol, G. -- On declassification and the non-disclosure policy -- Computer Security Foundation Workshop, 2005, pp. 226-240.

[ html ]

[Alm05]

Almeida Matos, A. -- Non-disclosure for distributed mobile code -- FST-TCS'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 max-plus quasi-interpretations -- Fundamenta Informaticae, 652005, pp. 29-60.

[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.

2004

[Bou04]

Boudol, G. -- Safe recursive boxes -- RR-5115, INRIA, February, 2004.

[ html ]

[Cia04]

Ciabrini, D. -- Debugging Scheme Fair Threads -- Proceedings of the 5th ACM-SIGPLAN Workshop on Scheme and Functional Programming, Snowbird, UT, USA, September, 2004, pp. 75-88.

[ http://www-sop.inria.fr/mimosa/fp/Bugloo ]

[Ama04]

Amadio, R. -- Synthesis of max-plus quasi-interpretations -- 18-2004, 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. 87-98.

[ http://www-sop.inria.fr/mimosa/Stephane.Epardaud/papers/ulm-scheme-2004.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 multi-threaded and distributed programming via strong mobility with a deterministic semantics. We present the multi-threading 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 real-life 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 Nice-Sophia 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. 203--214.

[ html ]

This paper presents Fair Threads, a new model for concurrent programming. This multi-threading 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 non-blocking 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 real-life 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 -- RR-5183, 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 SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan, 2004.

We prove the decidability of the quantifier-free, 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. -- History-Dependent 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. 263-315.

[ 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. 68--82.

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 first-order 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 quasi-interpretation. 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. 234-248.

[ 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. 265--279.

We define a simple stack machine for a first-order 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 quasi-interpretations 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. 126--144.

[ pdf ]

[ACD04b]

2003

[CDG03]

Charatonik, W. et al. -- Model Checking Mobile Ambients -- Theoretical Computer Science, 308(1), Nov, 2003, pp. 277--331.

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 replication-free calculus and guarantee-free logic we prove that the problem is PSPACE-complete. 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 PSPACE-hardness of the problem for several quite simple fragments of the calculus and the logic; this suggests that there are no interesting fragments with polynomial-time model checking algorithms.

[Aco03]

Acosta-Bermejo, R. -- Rejo - Langage d'objets réactifs et d'agents -- Thèse de doctorat de l'ENSMP, Oct, 2003.

[ ftp://ftp-sop.inria.fr/mimosa/rp/bibliography/These-RaulACOSTA.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://www-sop.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. 839--886.

[ ps.gz ]

This paper presents Biglook, a widget library for an extended version of the Scheme programming language. It uses classes of a Clos-like object layer to represent widgets and Scheme closures to handle graphical events. Combining functional and object-oriented programming styles yields an original application programming interface that advocates a strict separation between the implementation of the graphical interfaces and the user-associated commands, enabling compact source code.

The Biglook implementation separates the Scheme programming interface and the native back-end. 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. 246--263.

[ http://www.cmi.univ-mrs.fr/ dalzilio/Papers/sheaves-xml.pdf ]

XML documents, and other forms of semi-structured 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 well-suited 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.techniques-ingenieur.fr ]

[TZH03]

Teller, D. and Zimmer, P. and Hirschkoff, D. -- Using ambients to control resources -- Schedae Informaticae, 122003, pp. 113--127.

[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. 60-74.

[ html ]

[Zim03]

Zimmer, P. -- On the expressiveness of pure safe ambients -- Mathematical Structures in Computer Science, 132003, pp. 721--770.

[ http://www-sop.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://www-sop.inria.fr/mimosa/personnel/Pascal.Zimmer/papers/express00.ps ]

[ABL03]

Amadio, R. and Boudol, G. and Lhoussaine, C. -- The receptive distributed pi-calculus -- TOPLAS, 25(5), 2003, pp. 549-577.

[ 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. 153--167.

[ http://www.cmi.univ-mrs.fr/ dalzilio/Papers/final-pbs.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.

2002

[DL02]

Dal Zilio, S. and Lugiez, D. -- XML Schema, Tree Logic and Sheaves Automata -- 4631, INRIA, Nov, 2002.

[ http://www.cmi.univ-mrs.fr/ dalzilio/Papers/RR-4631.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 semi-structured 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 associative-commutative operator in the schema language, inherited from the &-operator of SGML, and the inherent limitations of regular tree automata in dealing with associative-commutative algebras. The class of automata considered here, called sheaves automata, is a tailored version of automata for unranked trees with both associative and associative-commutative 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 Scheme-to-C 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 just-in-time 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. 85--97.

[ 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 -- 08-2002, LIF, Jun, 2002.

[ http://www.cmi.univ-mrs.fr/ dalzilio/Papers/rrlif-08-2002.ps ]

We describe multitree automata and a related logic on multitrees. Multitrees are extensions of trees with both associative and associative-commutative 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 associative-commutative operators, determinisation, decidability of the test for emptiness, ... We apply our automata to query languages for XML-like 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 XML-like document. This proposition has the same flavour as a query language for semi-structured recently proposed by Cardelli and Ghelli. The same tree logic is used to yield decidable cases of inductive reducibility modulo associativity-commutativity, a key property in inductive theorem proving based on rewriting.

[DG02]

Dal Zilio, S. and Gordon, A. -- Region analysis and a pi-calculus with groups -- Journal of Functional Programming, 12(3), May, 2002, pp. 229--292.

We show that the typed region calculus of Tofte and Talpin can be encoded in a typed pi-calculus 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 de-allocated 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 pi-calculus, each name has a statically determined group to which it belongs. Groups allow for type-checking 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 co-inductive formulation. We prove the encoding preserves the static and dynamic semantics of the region calculus. Our proof of the correctness of region de-allocation shows it to be a specific instance of a general garbage collection principle for the pi-calculus with effects. We propose new equational laws for letregion, analogous to scope mobility laws in the pi-calculus, 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. 288--303.

[ http://www-sop.inria.fr/mimosa/personnel/Pascal.Zimmer/papers/concur02.ps ]

[Zim02]

Zimmer, P. -- On the expressiveness of pure safe ambients -- INRIA Research Report RR-4350, 2002.

[ http://www-sop.inria.fr/mimosa/personnel/Pascal.Zimmer/papers/RR-4350.ps ]

[BZ02]

Boudol, G. and Zimmer, P. -- Recursion in the call-by-value lambda-calculus -- Proceedings of FICS 2002 (Fixed Points in Computer Science), BRICS Notes Series NS-02-2, 2002.

[ http://www-sop.inria.fr/mimosa/personnel/Pascal.Zimmer/papers/fics02.ps ]

[ABL02]

Amadio, R. and Boudol, G. and Lhoussaine, C. -- On message deliverability and non-uniform receptivity -- Fundamenta Informaticae, 53(2), 2002, pp. 105-130.

[ html ]

[TZH02b]

Teller, D. and Zimmer, P. and Hirschkoff, D. -- Using ambients to control resources -- LIP Research Report N. 2002-16, ENS Lyon, 2002.

[ http://www-sop.inria.fr/mimosa/personnel/Pascal.Zimmer/papers/RR2002-16.ps ]

[BC02]

Boudol, G. and Castellani, I. -- Non-interference for concurrent programs and thread systems -- Theoretical Computer Science, 281(1), 2002, pp. 109-130.

[ html ]

[BC02b]

Boudol, G. and Castellani, I. -- Noninterference for Concurrent Programs and Thread Systems -- Theoretical Computer Science, 281(1), 2002, pp. 109-130.

2001

[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.univ-mrs.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. 206--222.

[ http://www.cmi.univ-mrs.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 pi-calculus, 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 -- MSR-TR-2001-03, Microsoft Research, May, 2001.

[ http://www.cmi.univ-mrs.fr/ dalzilio/Papers/tr-2001-03.ps ]

We settle the complexity bounds of the model checking problem for the replication-free ambient calculus with public names against the ambient logic without parallel adjunct. We show that the problem is PSPACE-complete. 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 PSPACE-hardness of the problem for several quite simple fragments of the calculus and the logic; this suggests that there are no interesting fragments with polynomial-time 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. 152--167.

[ http://www.cmi.univ-mrs.fr/ dalzilio/Papers/fossacs2001.pdf ]

[BC01]

Boudol, G. and Castellani, I. -- Noninterference for Concurrent Programs -- ICALP'01, Lecture Notes in Computer Science, (2076), 2001, pp. 382-395.

[Cas01]

Castellani, I. -- Process Algebras with Localities -- North-Holland, Amsterdam, 2001, pp. 945-1045.

[I. 01]

I. Castellani, -- Process Algebras with Localities -- North-Holland, Amsterdam, 2001, pp. 945-1045.

[BSD01]

Boussinot, F. et al. -- A reactive behavior framework for dynamic virtual worlds -- Web3D, 2001, pp. 69--75.

2000

[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. 245--256.

[ 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 Sophia-Antipolis, Route des Colles, B.P. 145 -- F-06903 Sophia-Antipolis, 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 \pi-calculus with groups -- MFCS 2000 -- 25th International Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, Aug, 2000, pp. 1--20.

[ http://www.cmi.univ-mrs.fr/ dalzilio/Papers/regions-mfcs.ps ]

We show that the typed region calculus of Tofte and Talpin can be encoded in a typed \pi-calculus 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 de-allocated 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 \pi-calculus, each name has a statically determined group to which it belongs. Groups allow for type-checking 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 co-inductive formulation. We prove the encoding preserves the static and dynamic semantics of the region calculus. Our proof of the correctness of region de-allocation shows it to be a specific instance of a general garbage collection principle for the \pi-calculus with effects. We propose new equational laws for \kwletregion, analogous to scope mobility laws in the \pi-calculus, and show them sound in our semantics.

[DG00b]

Dal Zilio, S. and Gordon, A. -- Region analysis and a \pi-calculus with groups -- MSR-TR-2000-57, Microsoft Research, Aug, 2000.

[ http://www.cmi.univ-mrs.fr/ dalzilio/Papers/tr-2000-57.ps ]

[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. 409--424.

[ http://www.cmi.univ-mrs.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 pi-calculus that directly contains the lambda calculus, with record and first-order 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 self-types and synchronization primitives. We also prove some equational laws on objects.

[Dal00b]

Dal Zilio, S. -- Spatial Congruence for the Ambients is Decidable -- MSR-TR-2000-41, Microsoft Research, May, 2000.

[ http://www.cmi.univ-mrs.fr/ dalzilio/Papers/tr-2000-41.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 edge-labelled finite-depth 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. 1--43.

[Ser00c]

Serrano, M. -- Bee: an Integrated Development Environment for the Scheme Programming Language -- Journal of Functional Programming, 10(2), May, 2000, pp. 1--43.

[ 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. -- \lambda-Calculus, Multiplicites and the \pi-Calculus -- 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. 545--566.

[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. 375--390.

[ http://www-sop.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 NS-00-2, 2000.

[ http://www-sop.inria.fr/mimosa/personnel/Pascal.Zimmer/papers/express00.ps ]