
[BD08b]  Boussinot, F. and Dabrowski, F.  Safe Reactive Programming: the FunLoft Proposal  Proc. of MULTIPROG  First Workshop on Programmability Issues for MultiCore 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.  Stateoriented 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 picalculus  Proceedings ACM SIGPLAN Principles and Practice of Declarative Programming , Jul, 2007, pp. 4555 . 
 
[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 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 ] 
 
[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 ComputerAided Design of Integrated Circuits and Systems, 26(3), Mar, 2007, pp. 456467. 
 
[TE07b]  Tardieu, O. and Edwards, S.  Instantaneous Transitions in Esterel  Proceedings of the Workshop on ModelDriven HighLevel 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. 121150 . 
 
[BD07c]  Boussinot, F. and Dabrowsky F.,  Formalisation of FunLoft  http://hal.inria.fr/inria00183242, Inria, 2007. 
 
[Bou07g]  Boussinot, F.  A Benchmark for Multicore Machines  http://hal.inria.fr/inria00174843, Inria, 2007. 
 
[Cas07d]  Castellani, I.  Stateoriented noninterference for CCS  ENTCS, 2007, pp. 3960. 
 [ ] 
 
[Ama07d]  Amadio, R.  A synchronous picalculus  Information and Computation. 205(9):14701490, 2007. 
 
[Bou07h]  Boussinot, F.  A Benchmark for Multicore Machines. http://hal.inria.fr/inria00174843  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/inria00183242  2007. 
 
[Dam06c]  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 ] 
 
[TE06b]  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. 
 
[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. 445469. 


 
[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/FLoC06/TVpreproceedings.pdf ] 
 
[RF06b]  Roberto M. Amadio, and FréDéRic Dabrowski,  Feasible Reactivity in a synchronous picalculus, 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. 445469. 


 
[BD06b]  Boussinot, F. and Dabrowski, F.  Secure Multicore Programming  2006. 
 
[Bou05f]  Boussinot, F.  Cyclone+Loft  September, 2005. 
 [ ftp://ftpsop.inria.fr/pub/rapports/RR5680.ps.gz ] 
 
[DG05c]  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. 

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

 
[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 TailRecursive 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 ACMSIGPLAN Workshop on Scheme and Functional Programming, Snowbird, UT, USA, September, 2004, pp. 7588. 
 [ http://wwwsop.inria.fr/mimosa/fp/Bugloo ] 
 
[Ama04b]  Amadio, R.  Synthesis of maxplus quasiinterpretations  182004, 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 NiceSophia 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  RR5183, 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 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. 

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

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

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

 
[Van04b]  Vanackere, V.  HistoryDependent 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. 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. 

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

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

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

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

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

 
[BC02d]  Boudol, G. and Castellani, I.  Noninterference for Concurrent Programs and Thread Systems  Theoretical Computer Science, 281(1), 2002, pp. 109130. 
 
[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.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. 

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

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

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

 
[BSD01b]  Boussinot, F. et al.  A reactive behavior framework for dynamic virtual worlds  Web3D, 2001, pp. 6975. 
 
[I. 01b]  I. Castellani,  Process Algebras with Localities  NorthHolland, Amsterdam, 2001, pp. 9451045. 
 
[Cas01b]  Castellani, I.  Process Algebras with Localities  NorthHolland, Amsterdam, 2001, pp. 9451045. 
 
[BC01b]  Boudol, G. and Castellani, I.  Noninterference for Concurrent Programs  ICALP'01, Lecture Notes in Computer Science, (2076), 2001, pp. 382395. 
 
[DG00c]  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. 

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

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

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

 
[Ser00d]  Serrano, M.  Bee: an Integrated Development Environment for the Scheme Programming Language  Journal of Functional Programming, 10(2), May, 2000, pp. 143. 
 
[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. 
 
