> > MimosaMigration and Mobility: Semantics and Applications

[BD08b]

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.

[BCH08b]

Boudol, G. et al. -- Twenty Years on: Reflections on the CEDISYS Project. Combining True Concurrency with Process Algebra -- Springer, 2008.

[Bou07f]

Boudol, G. -- Définition d'une machine abstraite pour ULM -- Livrable D1.1, CRE 46136511, Juin, 2007.

[ABD07b]

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.

[Cas07c]

Castellani, I. -- State-oriented noninterference for CCS -- 6322, INRIA, 10, 2007.

[ ]

[BCM07b]

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.

[Loi07b]

Loitsch, F. -- Exceptional Continuations in JavaScript -- 2007 Workshop on Scheme and Functional Programming, Freiburg, Germany, Sep, 2007.

[AD07b]

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 .

[AP07b]

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.

[LS07d]

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 ]

[Tar07b]

Tardieu, O. -- A deterministic logical semantics for pure Esterel -- ACM Transactions on Programming Languages and Systems, 29(2), Apr, 2007, pp. 8.

[STE07b]

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.

[TE07b]

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.

[Ama07c]

Amadio, R. -- The SL synchronous language, revisited -- Journal of Logic and Algebraic Programming , 70 Feb, 2007, pp. 121-150 .

[BD07c]

Boussinot, F. and Dabrowsky F., -- Formalisation of FunLoft -- http://hal.inria.fr/inria-00183242, Inria, 2007.

[Bou07g]

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

[Cas07d]

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

[ ]

[Ama07d]

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

[Bou07h]

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

[Dab07b]

Dabrowsky, F. -- Programmation Réactive Synchrone: langages et contrôle des ressources -- Université Paris 7, 2007.

[BD07d]

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

[Dam06c]

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 ]

[TE06b]

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.

[SGL06c]

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 ]

[Bou06i]

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.

[DB06b]

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 ]

[RF06b]

Roberto M. Amadio, and FréDéRic Dabrowski, -- Feasible Reactivity in a synchronous pi-calculus, Draft -- 2006.

[Dam06d]

Damien Ciabrini, -- Stack Filtering for Source Level Debugging -- To appear in Software: Practice and Experience, 2006.

[Bou06j]

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.

[BD06b]

Boussinot, F. and Dabrowski, F. -- Secure Multicore Programming -- 2006.

[Bou05f]

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

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

[DG05c]

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.

[ABD05b]

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.

[ABB05f]

Amadio, R. et al. -- Reactive concurrent programming revisited -- Bertinoro, Aug, 2005.

[ pdf ]

[AD05b]

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.

[DG05d]

Dal Zilio, S. and Gascon, R. -- Resource Bound Certification for a Tail-Recursive Virtual Machine -- 26, LIF, Jun, 2005.

[Dam05b]

Damien Ciabrini, -- Stack virtualization for source level debugging -- John Wiley & Sons, Ltd, 2005.

[DB05b]

Dabrowsky, F. and Boussinot, F. -- Cooperative Threads and Preemptive Computations -- 2005.

[Cia04b]

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 ]

[Ama04b]

Amadio, R. -- Synthesis of max-plus quasi-interpretations -- 18-2004, LIF, Marseille, France, January, 2004.

[C. 04b]

C. Brunette, -- Construction et simulation graphiques de comportements: le modèle des Icobjs -- Thèse de doctorat, Université de Nice-Sophia Antipolis, Oct, 2004.

[Tar04d]

Tardieu, O. -- Loops in Esterel: from operational semantics to formally specified compilers -- Ecole des Mines de Paris, Sep, 2004.

[Tar04e]

Tardieu, O. -- A deterministic logical semantics for Esterel -- Proceedings of the Workshop on Structural Operational Semantics, London, United Kingdom, Aug, 2004.

[Bou04k]

Boussinot, F. -- Reactive Programming of Cellular Automata -- RR-5183, Inria, May, 2004.

[Tar04f]

Tardieu, O. -- Goto and Concurrency: Introducing Safe Jumps in Esterel -- Proceedings of the Workshop on Synchronous Languages, Applications, and Programming, Barcelona, Spain, Mar, 2004.

[DL04b]

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.

[ACD04c]

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.

[Dab04c]

Dabrowski, F. -- Reactivity in ULM -- 2004.

[Dab04d]

Dabrowski, F. -- Side effects and polynomial bounds -- 2004.

[Bou04l]

Boussinot, F. -- Concurrent Programming with Fair Threads -- The LOFT Language -- 2004.

[ html | pdf ]

[Zim04b]

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 ]

[ACD04d]

[AD04b]

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.

[Van04b]

Vanackere, V. -- History-Dependent Scheduling for Cryptographic Processes -- Proc. VMCAI' 2004, Lecture Notes in Computer Science, Venice, Italy, 2004.

[CDG03b]

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.

[Aco03b]

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 ]

[DL03b]

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.

[Gua03b]

Guan, X. -- Towards a tree of channels -- Electronic Notes in Theoretical Computer Science, 2003.

[DF03b]

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.

[DL02c]

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.

[DL02d]

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.

[DG02b]

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.

[BC02d]

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

[Dal01c]

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.

[Dal01d]

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.

[CDG01c]

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.

[CDG01d]

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 ]

[BSD01b]

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

[I. 01b]

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

[Cas01b]

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

[BC01b]

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

[DG00c]

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 ]

[Dal00c]

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.

[DG00d]

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.

[Dal00d]

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.

[Ser00d]

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

[Bou00d]

Boussinot, F. -- Objets réactifs en Java -- Collection Scientifique et Technique des Telecommunications, PPUR, 2000.

[Bou00e]

Boussinot, F. -- Objets réactifs en Java -- Presses Polytechniques Universitaires Romandes, 2000.