=======================================================================
= Bibtex file automatically generated on Fri Apr 26 11:04:42 CEST 2024 =
=======================================================================

-------------
- Articles  -
-------------

@Article\{damiani.etal:on-reclassification-multithreading,
  author = \{F. Damiani and M. {Dezani-Ciancaglini} and P. Giannini},
  title = \{On Re-classification and Multithreading},
  Abstract = \{In this paper we consider re-classification in the presence of 
              multi-threading. To this aim we define a multi-threaded 
              extension of the language Fickle, that we call FickleMT. We 
              define an operational semantics and a type and effect system for 
              the language. Each method signature carries the information on 
              the possible effects of the method execution. The type and 
              effect system statically checks this information. The 
              operational semantics uses this information in order to delay 
              the execution of some threads when this could cause access to 
              non-existing members of objects. We show that in the execution 
              of a well-typed expression such delays do not produce deadlock. 
              Lastly we discuss a translation from FickleMT into Java, showing 
              how the operational semantics can be implemented with the 
              standard Java multi-threading constructs.},
  journal = \{JOT-04},
  year = \{2004}, 
  volume = \{3}, 
  number = \{11}, 
  pages = \{5-30}, 
  url = \{http://mikado.di.fc.ul.pt/repository/damiani.etal_on-reclassification-multithreading.pdf}
}

@Article\{stefani:calculus-kells,
  author = \{J.B. Stefani},
  title = \{A Calculus of Kells},
  Abstract = \{This paper introduces the Kell calculus, a new process calculus
              that retains the original insights of the M-calculus (local actions,
              higher-order processes and programmable membranes) in a much simpler
              setting. The calculus is shown expressive enough to provide a direct
              encoding of several recent distributed process calculi such as Mobile
              Ambients and the Distributed Join calculus.},
  journal = \{ENTCS},
  year = \{2003}, 
  volume = \{85}, 
  number = \{1}, 
  url = \{http://mikado.di.fc.ul.pt/repository/stefani_calculus-kells.ps}
}

@Article\{boreale.gorla:process-calculi-verification,
  author = \{M. Boreale and D. Gorla},
  title = \{Process calculi and the verification of security protocols},
  Abstract = \{Recently there has been much interest towards using formal methods
              in the analysis of security protocols. Some recent approaches take
              advantage of concepts and techniques from the field of process calculi.
              Process calculi can be given a formal yet simple semantics, which
              permits rigorous definitions of such concepts as `attacker', `secrecy'
              and `authentication'. This feature has led to the development of solid
              reasoning methods and verification techniques, a few of which we outline
              in this paper.},
  journal = \{Journal of Telecommunications and Information Technology},
  year = \{To appear}, 
  url = \{http://mikado.di.fc.ul.pt/repository/boreale.gorla_process-calculi-verification.pdf}
}

@Article\{nicola.gorla.pugliese:confining-data-processes-gc-applications,
  author = \{R. {De Nicola} and D. Gorla and R. Pugliese},
  title = \{Confining Data and Processes in Global Computing Applications},
  Abstract = \{A programming notation is introduced that can be used for
	      protecting secrecy and integrity of data in global computing
	      applications. The approach is based on the explicit annotations of
	      data and network nodes. Data are tagged with information about the
	      allowed movements, network nodes are tagged with information about
	      the nodes that can send data and spawn processes to them. The
	      annotations are used to confine movements of data and
	      processes. The approach is illustrated by applying it to three
	      paradigmatic calculi for global computing, namely cKLAIM (a
	      calculus at the basis of KLAIM), Dpi (a distributed version of
	      the pi-calculus) and Mobile Ambients Calculus. For all of these
	      formalisms, it is shown that their semantics guarantees that
	      computations proceed only while respecting confinement
	      constraints. Namely, it is proven that, after successful static
	      type checking, data can reside at and cross only authorised nodes.
	      `Local' formulations of this property where only relevant
	      sub-nets type check are also presented. Finally, the theory is
	      tested by using it to model secure behaviours of a UNIX-like
	      multiuser system.},
  journal = \{Science of Computer Programming},
  year = \{2004}, 
  pages = \{Elsevier}, 
  url = \{http://mikado.di.fc.ul.pt/repository/nicola.gorla.pugliese_confining-data-processes-gc-applications.pdf}
}

@Article\{de-nicola.loreti:modal-logic-mobile-agents,
  author = \{R. {De Nicola} and M. Loreti},
  title = \{A Modal Logic for Mobile Agents},
  Abstract = \{KLAIM is an experimental programming language that supports a
              programming paradigm where both processes and data can be moved across
              different computing environments. The language relies on the use of
              explicit localities. This paper presents a temporal logic for specifying
              properties of Klaim programs. The logic is inspired by Hennessy-Milner
              Logic (HML) and the µ calculus, but has novel features that permit dealing
              with state properties and impact of actions and movements over the different
              sites. The logic is equipped with a complete proof system that enables one
              to prove properties of mobile systems.},
  journal = \{ACM Transactions on Computational Logic},
  year = \{To appear}, 
  url = \{http://mikado.di.fc.ul.pt/repository/de-nicola.loreti_modal-logic-mobile-agents.pdf}
}

@Article\{guan:towards-tree,
  author = \{X. Guan},
  title = \{Towards A Tree of Channels},
  Abstract = \{This paper presents a generalization of distributed $pi$-calculi to
              support a hierarchy of locations. We add nested locations on top
              of a $pi$-calculus core. By unifying channels and locations, we
              arrive at a computation model which uses mobile agents to pass
              addresses among immobile and nested locations. We choose a static
              binding semantics of addresses to enable easy navigation of mobile
              agents in the location tree. We support dynamic creation of new
              locations and garbage-collection of empty ones. A sample typed
              calculus is presented to demonstrate the formalization of type
              systems and related proof techniques in this calculus.},
  journal = \{ENTCS},
  year = \{2003}, 
  volume = \{85}, 
  number = \{1}, 
  url = \{http://mikado.di.fc.ul.pt/repository/guan_towards-tree.pdf}
}

------------------
- InProceedings  -
------------------

@InProceedings\{matos.boudol.castellani:typing-noninterference-reactive-programs,
  author = \{A. Matos and G. Boudol and I. Castellani},
  title = \{Typing noninterference for reactive programs},
  Abstract = \{We propose a type system to enforce the security property of {\em 
	      noninterference} in a core reactive language, obtained by extending 
              the imperative language of Volpano, Smith and Irvine with reactive 
              primitives that manipulate broadcast signals, as well as with a form 
              of ``scheduled'' parallelism. Due to the particular nature of
              reactive computations, the definition of noninterference has to be
              adapted. We give a formulation of noninterference based on bisimulation. 
              Our type system is inspired by that introduced by Boudol and Castellani, 
              and independently by Smith, to cope with nontermination and time leaks 
              in a language for parallel programs with scheduling. We establish the 
              soundness of this type system with respect to our notion of 
              noninterference.},
  booktitle = \{Foundations of Computer Security},
  year = \{2004}, 
  url = \{http://mikado.di.fc.ul.pt/repository/matos.boudol.castellani_typing-noninterference-reactive-programs.pdf}
}

@InProceedings\{ravara.etal:lsd-wysiwyg,
  author = \{A. Ravara and A. Matos and V. Vasconcelos and L. Lopes},
  title = \{Lexically scoping distribution: what you see is what you get},
  Abstract = \{We define a lexically scoped, asynchronous and distributed pi-calculus, with local
              communication and process migration. This calculus adopts the network-awareness
              principle for distributed programming and follows a simple model of distribution
              for mobile calculi: a lexical scope discipline combines static scoping with
              dynamic linking, associating channels to a fixed site throughout computation. 
              This discipline provides for both remote invocation and process migration. A 
              simple type system is a straightforward extension of that of the pi-calculus, 
              adapted to take into account the lexical scope of channels. An equivalence law 
              captures the essence of this model: a process behavior depends on the channels
              it uses, not on where it runs.},
  booktitle = \{FGC: Foundations of Global Computing},
  year = \{2003}, 
  volume = \{85(1)}, 
  series = \{ENTCS}, 
  publisher = \{Elsevier}, 
  url = \{http://mikado.di.fc.ul.pt/repository/ravara.etal_lsd-wysiwyg.pdf}
}

@InProceedings\{schmitt.stefani:the-m-calculus,
  author = \{A. Schmitt and J.B. Stefani},
  title = \{The M-calculus: A Higher-Order Distributed Process Calculus},
  Abstract = \{This paper presents a new distributed process calculus, called the
              M-calculus, that can be understood as a higher-order version of the
              Distributed Join calculus with programmable localities. The calculus
              retains the implementable character of the Distributed Join calculus
              while overcoming several important limitations: insufficient control
              over communication and mobility, absence of dynamic binding, and limited 
              locality semantics. The calculus is equipped with a polymorphic type 
              system that guarantees the unicity of locality names, even in presence 
              of higher-order communications -- a crucial property for the determinacy 
              of message routing in the calculus.},
  booktitle = \{Proceedings 30th Annual ACM Symposium on Principles of Programming Languages (POPL)},
  year = \{2003}, 
  url = \{http://mikado.di.fc.ul.pt/repository/schmitt.stefani_the-m-calculus.pdf}
}

@InProceedings\{vallecillo.vasconcelos.ravara:typing-behavior-objects,
  author = \{A. Vallecillo and V. Vasconcelos and A. Ravara},
  title = \{Typing the Behavior of Objects and Components using Session Types},
  Abstract = \{This paper describes a proposal for typing the behavior of
              objects in component models. Most component models, CORBA in 
              particular, do not offer any support for expressing behavior 
              al properties of objects beyond the ``static' information 
              provided by IDLs. We build on the works by Honda et al. and
              Gay and Hole to show how session types can be effectively used
              for describing protocols, extending the information currently
              provided by object interfaces. We show how session types not
              only allow high level specifications of complex object interactions,
              but also allow the definition of powerful interoperability tests
              at the protocol level, namely compatibility and substitutability
              of objects.},
  booktitle = \{1st International Workshop on Foundations of Coordination Languages
               and Software Architectures (Foclasa 2002)},
  year = \{2002}, 
  publisher = \{Elsevier Science Publishers}, 
  url = \{http://mikado.di.fc.ul.pt/repository/vallecillo.vasconcelos.ravara_typing-behavior-objects.pdf}
}

@InProceedings\{braghin.gorla.sassone:distributed-calculus-role-based,
  author = \{C. Braghin and D. Gorla and V. Sassone},
  title = \{A Distributed Calculus for Role-Based Access Control},
  Abstract = \{Role-based access control (RBAC) is increasingly attracting attention
	      because it reduces the complexity and cost of security administration
	      by interposing the notion of role in the assignment of
	      permissions to users.  
	      In this paper, we present a formal framework relying on an extension
	      of the pi-calculus to study the behavior of concurrent systems in a RBAC
	      scenario. We define a type system ensuring that the specified policy
	      is respected during computations, and a bisimulation to equate
	      systems.
	      The theory is then applied to three meaningful examples, namely finding
	      the `minimal' policy to run a given system, refining a system to
	      be run under a given policy (whenever possible), and minimizing the number 
	      of users in a given system without changing the overall behavior.},
  booktitle = \{Proceedings of 17th Computer Security Foundations Workshop (CSFW'04)},
  year = \{2004}, 
  pages = \{48--60}, 
  publisher = \{IEEE Computer Society}, 
  url = \{http://mikado.di.fc.ul.pt/repository/braghin.gorla.sassone_distributed-calculus-role-based.pdf}
}

@InProceedings\{lhoussaine.sassone:dependently-typed-ambient-calculus,
  author = \{C. Lhoussaine and V. Sassone},
  title = \{A Dependently Typed Ambient Calculus},
  Abstract = \{The Ambient calculus is a successful model of distributed, mobile
              computation, and has been the vehicle of new ideas for resource
              access control. Mobility types have been used to enforce
              elementary access control policies, expressed indirectly via
              classification of ambients in groups by means of  group types.
              The paper presents a theory of dependent types for the Ambient
              calculus which allows greater flexibility, while keeping the
              complexity away from the programmer into the type system.},
  booktitle = \{Proceedings of European Symposium on Programming, ESOP 03},
  year = \{2003}, 
  volume = \{2772}, 
  series = \{LNCS}, 
  publisher = \{Springer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/lhoussaine.sassone_dependently-typed-ambient-calculus.pdf}
}

@InProceedings\{gorla.hennessy.sassone:security-policies-membranes-gc,
  author = \{D. Gorla and M. Hennessy and V. Sassone},
  title = \{Security Policies as Membranes in Systems for Global Computing},
  Abstract = \{We propose a simple global computing framework, whose main concern is
              code migration. Systems are structured in sites, and each site is
              divided into  two parts: a computing body, and a membrane which
              regulates the interactions between the computing body and the
              external environment.
              More precisely, membranes are filters which control access to the
              associated site, and they also rely on the well-established notion of
              trust between sites.
              We develop a basic theory to express and enforce security
              policies via membranes. Initially, these only control the actions
              incoming agents intend to perform locally.  
              We then adapt the basic theory to encompass more sophisticated
              policies, where the number of actions an agent wants to perform, and
              also their order, are considered.},
  booktitle = \{Proceedings of 3rd EATCS Workshop on Foundations of Global Ubiquitous Computing (FGUC'04)},
  year = \{2004}, 
  series = \{ENTCS}, 
  publisher = \{Elsevier}, 
  url = \{http://mikado.di.fc.ul.pt/repository/gorla.hennessy.sassone_security-policies-membranes-gc.pdf}
}

@InProceedings\{gorla.pugliese:controlling-data-movement,
  author = \{D. Gorla and R. Pugliese},
  title = \{Controlling Data Movement in Global Computing Applications},
  Abstract = \{We present a programming notation aiming at protecting the secrecy
              of both host and agent data in global computing applications. The approach
              exploits annotations with sets of node addresses, called regions. A datum can be
              annotated with a region that specifies the network nodes that are allowed to interact
              with it. Network nodes come equipped with two region annotations specifying the nodes
              that can send data and spawn processes over them. The language semantics guarantees
              that computation proceeds according to these region constraints. To minimize the 
              overhead of runtime checks, a static compilation phase is exploited. The proposed 
              approach is largely independent of a specific programming language; however, to put
              it in concrete form, here we focus on its integration within the process language
              muKlaim. We prove that in compiled muKlaim nets, data can be manipulated only by
              authorized users. We also give a more local formulation of this property, where only
              a subnet is compiled. Finally, we use our theory to model the secure behaviour of a
              UNIX-like multiuser system.},
  booktitle = \{Proc. of 19th Annual ACM-SIGAPP Symposium on Applied Computing (SAC 04)},
  year = \{2004}, 
  publisher = \{ACM Press}, 
  url = \{http://mikado.di.fc.ul.pt/repository/gorla.pugliese_controlling-data-movement.pdf}
}

@InProceedings\{gorla.pugliese:resource-access-mobility-control,
  author = \{D. Gorla and R. Pugliese},
  title = \{Resource Access and Mobility Control with Dynamic Privileges Acquisition},
  Abstract = \{muKlaim is a process language that permits programming distributed
              systems made up of several mobile components interacting through multiple distributed
              tuple spaces. We present the language and a type system for controlling the activities,
              e.g. access to resources and mobility, of the processes in a net. By dealing with
              privileges acquisition, the type system enables dynamic variations of security policies.
              We exploit a combination of static and dynamic type checking, and of in-lined reference
              monitoring, to guarantee absence of run-time errors due to lack of privileges and state
              two type soundness results: one involves whole nets, the other is relative to subnets of
              larger nets.},
  booktitle = \{Proc. of 30th International Colloquium on Automata, Languages and Programming (ICALP 03)},
  year = \{2003}, 
  pages = \{119--132}, 
  volume = \{2719}, 
  series = \{LNCS}, 
  publisher = \{Springer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/gorla.pugliese_resource-access-mobility-control.pdf}
}

@InProceedings\{gorla.pugliese:enforcing-security-types,
  author = \{D. Gorla and R. Pugliese},
  title = \{Enforcing Security Policies via Types},
  Abstract = \{Security is a key issue for distributed systems/applications with
              code mobility, like, e.g., e-commerce and on-line bank transactions. In a scenario
              with code mobility, traditional solutions based on cryptography cannot deal with all
              security issues and additional mechanisms are necessary. In this paper, we present
              a flexible and expressive type system for security for a calculus of distributed and
              mobile processes. The type system has been designed to supply real systems security
              features, like the assignment of different privileges to users over different
              data/resources. Type soundness is guaranteed by using a combination of static and
              dynamic checks, thus enforcing specific security policies on the use of resources.
              The usefulness of our approach is shown by modeling the simplified behaviour of a
              bank account management system.},
  booktitle = \{Proc. of 1st Intern.Conf. on Security in Pervasive Computing (SPC 03)},
  year = \{2003}, 
  pages = \{88--103}, 
  volume = \{2802}, 
  series = \{LNCS}, 
  publisher = \{Springer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/gorla.pugliese_enforcing-security-types.pdf}
}

@InProceedings\{teller.zimmer.hirschkoff:using-ambients-control-resources,
  author = \{D. Teller and P. Zimmer and D. Hirschkoff},
  title = \{Using Ambients to Control Resources},
  Abstract = \{Current software and hardware systems, being parallel and
              reconfigurable, raise new safety and reliability problems, and the
              re-solution of these problems requires new methods. Numerous proposals
              attempt at reducing the threat of bugs and preventing several kinds of
              attacks. In this paper, we develop an extension of the calculus of
              Mobile Ambients, named Controlled Ambients, that is suited for
              expressing such issues, specifically Denial of Service attacks. We
              present a type system for Controlled Ambients, which makes resource
              control possible in our setting.},
  booktitle = \{Proceedings of CONCUR 2002 -- Concurrency Theory},
  year = \{2002}, 
  pages = \{288--303}, 
  volume = \{2421}, 
  series = \{Lecturer notes in computer science}, 
  publisher = \{Springer Verlag}, 
  url = \{http://mikado.di.fc.ul.pt/repository/teller.zimmer.hirschkoff_using-ambients-control-resources.pdf}
}

@InProceedings\{barbanera.etal:calculus-bounded-capacities-asian03,
  author = \{F. Barbanera and M. Bugliesi and M. {Dezani-Ciancaglini} and V. Sassone},
  title = \{A Calculus of Bounded Capacities},
  Abstract = \{Resource control has attracted increasing interest in foundational research on
              distributed systems. This paper focuses on space control and develops an analysis
              of space usage in the context of an ambient-like calculus with bounded capacities
              and weighed processes, where migration and activation require space. A type system
              complements the dynamics of the calculus by providing static guarantees that the
              intended capacity bounds are preserved throughout the computation.},
  booktitle = \{ASIAN 03},
  year = \{2003}, 
  pages = \{205--223}, 
  volume = \{2896}, 
  series = \{LNCS}, 
  publisher = \{Springer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/barbanera.etal_calculus-bounded-capacities-asian03.pdf}
}

@InProceedings\{damiani.etal:reclassification-multithreading-fickle-mt,
  author = \{F. Damiani and M. {Dezani-Ciancaglini} and P. Giannini},
  title = \{Re-classification and Multi-threading: Fickle MT},
  Abstract = \{In this paper we consider re-classification in the presence of 
              multi-threading. To this aim we define a multi-threaded 
              extension of the language Fickle, that we call FickleMT. 
              We define an operational semantics and a type and effect system
              for the language. Each method signature carries the information 
              on the possible effects of the method execution. The type and 
              effect system statically checks this information. The 
              operational semantics uses this information in order to delay 
              the execution of some threads when this could cause 
              messageNotUnderstood errors. We prove that in the execution of a 
              well-typed expression such delays do not produce deadlock.},
  booktitle = \{SAC-2004},
  year = \{2004}, 
  publisher = \{ACM}, 
  url = \{http://mikado.di.fc.ul.pt/repository/damiani.etal_reclassification-multithreading-fickle-mt.pdf}
}

@InProceedings\{germain.lacoste.stefani:abstract-machine-m-calculus,
  author = \{F. Germain and M. Lacoste and J.-B. Stefani},
  title = \{An Abstract Machine for a Higher-Order Distributed Process Calculus},
  Abstract = \{This paper  presents the formal  specification of an  abstract machine
              for the M-calculus, a new distributed process calculus. The M-calculus 
              can be understood as an extension  of the join-calculus that realizes an
              original combination of the following features: programmable localities,
              higher-order functions and processes, process mobility, and dynamic
              binding. Our abstract machine covers these  different features and presents
              a modular structure that clearly separates the sequential (functional)
              evaluation  mechanism from the execution core, and the latter from basic
              marshalling, location and routing mechanisms.},
  booktitle = \{EATCS Workshop on Foundations of Wide Area Network Computing (FWAN'02)},
  year = \{2002}, 
  volume = \{66.3}, 
  publisher = \{Elsevier}, 
  url = \{http://mikado.di.fc.ul.pt/repository/germain.lacoste.stefani_abstract-machine-m-calculus.pdf}
}

@InProceedings\{martins.ravara:typing-migration-control-lsdpi,
  author = \{F. Martins and A. Ravara},
  title = \{Typing Migration Control in Lsdpi},
  Abstract = \{This paper presents a type system to control the migration of code
              between sites in a concurrent distributed framework. The type system 
              constitutes a decidable mechanism to ensure specific security policies, 
              which control remote communication, process migration, and channel 
              creation. The approach is as follows: each network administrator 
              specifies sites privileges, and a type system checks that the processes 
              running at those sites, as well as the composition of the sites, respect 
              these policies. At runtime, well-typed networks do not violate the 
              security policies declared for each site.},
  booktitle = \{Proceedings of FCS'04},
  year = \{2004}, 
  pages = \{1--12}, 
  volume = \{31}, 
  publisher = \{Turku Centre for Computer Science}, 
  url = \{http://mikado.di.fc.ul.pt/repository/martins.ravara_typing-migration-control-lsdpi.pdf}
}

@InProceedings\{martins.lopes.vasconcelos:impact-linearity-information,
  author = \{F. Martins and L. Lopes and V. Vasconcelos},
  title = \{The Impact of Linearity Information on the Performance of TyCO},
  Abstract = \{We describe a linear channel inference system for the TyCO
              programming language, where channel usage is tracked through
              method invocations as well as procedure calls. We then apply 
              linear channel information to optimize code generation for a 
              multithreaded runtime system. The impact in terms of speed 
              and space is analyzed.},
  booktitle = \{Workshop on Types in Programming (TIP'02)},
  year = \{2002}, 
  publisher = \{Elsevier Science Publishers}, 
  url = \{http://mikado.di.fc.ul.pt/repository/martins.lopes.vasconcelos_impact-linearity-information.pdf}
}

@InProceedings\{boudol:generic-membrane-model,
  author = \{G. Boudol},
  title = \{A generic membrane model},
  Abstract = \{In this note we introduce a generic model for controlling migration in 
              a network of distributed processes. To this end, we equip the membrane of 
              a domain containing processes with some computing power, including in 
              particular some specific primitives to manage the movements of entities 
              from the inside to the outside of a domain, and conversely. We define a 
              pi-calculus instance of our model, and illustrate by means of examples its
              expressive power. We also discuss a possible extension of our migration
              model to the case of hierarchically organized domains.},
  booktitle = \{Second Global Computing Workshop},
  year = \{2004}, 
  url = \{http://mikado.di.fc.ul.pt/repository/boudol_generic-membrane-model.pdf}
}

@InProceedings\{boudol:UML-core-programming-model,
  author = \{G. Boudol},
  title = \{ULM: a core programming model for global computing},
  Abstract = \{We propose a programming model to address the
              unreliable character of accessing resources in a global computing
              context, focusing on giving a precise semantics for a small, yet
              expressive core language. To design the language, we use ideas and
              programming constructs from the synchronous programming style, that
              allow us to deal with the suspensive character of some operations, and
              to program reactive behaviour. We also introduce constructs for
              programming mobile agents, that move together with their state, which
              consists of a control stack and a store. This makes the access to
              references also potentially suspensive.},
  booktitle = \{ESOP 04},
  year = \{2004}, 
  url = \{http://mikado.di.fc.ul.pt/repository/boudol_UML-core-programming-model.pdf}
}

@InProceedings\{boudol.zimmer:type-inference-intersection-type-discipline,
  author = \{G. Boudol and P. Zimmer},
  title = \{On type inference in the intersection type discipline},
  Abstract = \{We introduce a new unification procedure for the type inference problem 
              in the intersection type discipline. We show that unification exactly 
              corresponds to reduction in an extended lambda-calculus, where one never 
              erases arguments that would be discarded by ordinary beta-reduction. We 
              show that our notion of unification allows us to compute a principal typing 
              for any strongly normalizing lambda-expression.},
  booktitle = \{ITRS'04 Workshop},
  year = \{2004}, 
  url = \{http://mikado.di.fc.ul.pt/repository/boudol.zimmer_type-inference-intersection-type-discipline.pdf}
}

@InProceedings\{paulino.marques.lopes.etal:async-lang,
  author = \{H. Paulino and P. Marques and L. Lopes and V. Vasconcelos and F. Silva},
  title = \{A Multi-Threaded Asynchronous Language},
  Abstract = \{We describe a reference implementation of a multi-threaded run-time 
              system for a core programming language based on a process calculus. The core
              language features processes running in parallel and communicating through 
              asynchronous messages as the fundamental abstractions. The programming style
              is fully declarative, focusing on the interaction patterns between processes. 
              The parallelism, implicit in the syntax of the programs, is effectively 
              extracted by the language compiler and explored by the run-time system.},
  booktitle = \{7th International Conference on Parallel Computing Technologies (PaCT 03)},
  year = \{2003}, 
  pages = \{316--323}, 
  volume = \{2763}, 
  series = \{LNCS}, 
  publisher = \{Springer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/paulino.marques.lopes.etal_async-lang.pdf}
}

@InProceedings\{acciai.boreale:xpi-process-calculus-xml,
  author = \{L. Acciai and M.Boreale},
  title = \{XPi: a typed process calculus for XML messaging},
  Abstract = \{We present XPi, a core calculus for XML messaging. XPi features 
              asynchronous communications, pattern matching, name and code 
              mobility, integration of static and dynamic typing. Flexibility 
              and expressiveness of this calculus are illustrated by a few 
              examples, some concerning description and discovery of web 
              services. In XPi, a type system disciplines XML message handling 
              at the level of channels, patterns and processes. A run-time 
              safety theorem ensures that in well-typed systems no service 
              will ever receive documents it cannot understand, and that the 
              offered services, even if re-defined, will comply with the 
              declared channel capacities.},
  booktitle = \{Proceedings of FMOODS05},
  year = \{2005}, 
  series = \{LNCS}, 
  publisher = \{Springer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/acciai.boreale_xpi-process-calculus-xml.pdf}
}

@InProceedings\{bettini:javapackage-class-mixinmobility-distributed-setting,
  author = \{L. Bettini},
  title = \{A Java package for class and mixin mobility in a distributed setting},
  Abstract = \{Mixins, i.e., classes parameterized over the superclass, can
              be the right mechanism for dynamically assembling class hierarchies
              with mobile code downloaded from different sources.  In this paper we
              present the Java package \texttt{momi} that implements the concepts of
              the language \textt{momi}, which is a calculus for exchanging mobile 
              object-oriented code structured through mixin inheritance.  This package 
              can be thought of as an ``assembly' language that should be the target 
              of a compiler for a mobile code object-oriented language. In order to 
              show an usage of the package, we illustrate how it is used by the compiler
              of \textsc{X-Klaim}, a programming language for mobile code where
              distributed processes can exchange classes and mixins through distributed 
              tuple spaces.},
  booktitle = \{Proceedings of FIDJI 03},
  year = \{2003}, 
  series = \{LNCS}, 
  publisher = \{Springer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/bettini_javapackage-class-mixinmobility-distributed-setting.pdf}
}

@InProceedings\{bettini.loreti.pugliese:Infrastructure-language-open-nets,
  author = \{L. Bettini and M. Loreti and R. Pugliese},
  title = \{An Infrastructure Language for Open Nets},
  Abstract = \{The structure of open nets, like the Internet, is highly dynamic, 
              as the topology of component networks continuously evolves. In this 
              context, node connectivity is a key aspect and a language for 
              distributed network-aware mobile applications should provide explicit 
              mechanisms to handle it. In this paper, we address the problem of 
              expressing dynamic changes of node connectivity at linguistic level 
              and, in particular, we focus on a slight extension of the language 
              KLAIM, that is targeted to this aim. The extension consists of the 
              introduction of a new category of processes that, in addition to the 
              standard process operations, can execute a few new coordination 
              operations for establishing new connections, accepting connection
              requests and removing connections. Our extension puts forward a clean
              separation between the coordinator level and the user level and, hence, 
              it is modular enough to be easily applicable also to other network-aware 
              languages. We will also show that our approach can be used as a guide for
              actual distributed (i.e. without a single centralized server) 
              implementations of mobile systems.},
  booktitle = \{Proceedings of ACM SAC 2002, Special Track on Coordination Models, Languages and Applications)},
  year = \{2002}, 
  pages = \{373--377}, 
  publisher = \{ACM}, 
  url = \{http://mikado.di.fc.ul.pt/repository/bettini.loreti.pugliese_Infrastructure-language-open-nets.pdf}
}

@InProceedings\{bettini.etal:sw-frame-rapid-prototyping-run-time-systems,
  author = \{L. Bettini and R. {De Nicola} and D. Falassi and M. Lacoste and L. Lopes and L. Oliveira and H. Paul},
  title = \{A Software Framework for Rapid Prototyping of Run-Time Systems for Mobile Calculi},
  Abstract = \{We describe the architecture and the implementation of the MIKADO
              software framework, that we call IMC (Implementing Mobile Calculi). The
              framework aims at providing the programmer with primitives to design 
              and implement run-time systems for distributed process calculi. 
              The paper describes the four main components of abstract machines for 
              mobile calculi (node topology, naming and binding, communication 
              protocols and mobility) that have been implemented as Java packages. 
              The paper also contains the description of a prototype implementation 
              of a run-time system for the Distributed Pi-Calculus relying
              on the presented framework},
  booktitle = \{Volume of Postproceedings of Global Computing Workshop (GC 04)},
  year = \{to apear}, 
  series = \{LNCS}, 
  publisher = \{Springer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/bettini.etal_sw-frame-rapid-prototyping-run-time-systems.pdf}
}

@InProceedings\{bettini.bono.venneri:oklaim-coordination-language-mobile-mixins,
  author = \{L. Bettini and V. Bono and B. Venneri},
  title = \{\textsc{O'Klaim}: a coordination language with mobile mixins},
  Abstract = \{This paper presents O'Klaim{} (Object-Oriented Klaim), a linguistic
              extension of the higher-order calculus for mobile processes Klaim
              with object-oriented features.  Processes interact by an
              asynchronous communication model: they can distribute and retrieve
              resources, sometimes structured as incomplete classes, i.e., mixins,
              to and from distributed tuple spaces.  This mechanism is coordinated
              by providing a subtyping relation on classes and mixins, which
              become polymorphic items during communication.  We propose a static
              typing system for: $(i)$ checking locally each process in its own
              locality; $(ii)$ decorating object-oriented code that is sent to
              remote sites with its type.  This way, tuples can be dynamically
              retrieved only if they match by subtyping with the expected type.
              If this pattern matching succeeds, the retrieved code can be
              composed with local code, dynamically and automatically, in a
              type-safe way.  Thus a global safety condition is guaranteed without
              requiring any additional information on the local reconfiguration of
              local and foreign code, and, in particular, without any further type
              checking.  Finally, we present main issues concerning the
              implementation of O'Klaim.},
  booktitle = \{Proceedings of COORDINATION'04},
  year = \{2004}, 
  pages = \{20--37}, 
  volume = \{2949}, 
  series = \{LNCS}, 
  publisher = \{Springer-Verlag}, 
  url = \{http://mikado.di.fc.ul.pt/repository/bettini.bono.venneri_oklaim-coordination-language-mobile-mixins.pdf}
}

@InProceedings\{bettini.bono.likavec:core-calculus-ho-mixins-classes,
  author = \{L. Bettini and V. Bono and S. Likavec},
  title = \{A Core Calculus of Higher-Order Mixins and Classes},
  Abstract = \{We present an object-oriented calculus based on \emph{higher-order} 
              mixin construction via \emph{mixin composition}, where some software 
              engineering requirements are modelled in a formal setting, allowing 
              to prove the absence of \emph{message-not-understood} run-time errors.},
  booktitle = \{Proceedings SAC, Special Track on Programming Languages, Poster Paper},
  year = \{2004}, 
  publisher = \{ACM}, 
  url = \{http://mikado.di.fc.ul.pt/repository/bettini.bono.likavec_core-calculus-ho-mixins-classes.pdf}
}

@InProceedings\{bettini.bono.likavec:core-calculus-hightorder-mixins-classes,
  author = \{L. Bettini and V. Bono and S. Likavec},
  title = \{A Core Calculus of Higher-Order Mixins and Classes},
  Abstract = \{This work presents an object-oriented calculus based on
              \emph{higher-order} mixin construction via \emph{mixin composition},
              where some software engineering requirements are modeled in a formal
              setting allowing to prove the absence of \emph{message-not-understood} 
              run-time errors.  Mixin composition is shown to be a valuable language 
              feature enabling a cleaner object-oriented design and development.  
              In what we believe being quite a general framework, we give directions
              for designing a programming language equipped with higher-order mixins,  
              although our study is not based on any already existing object-oriented 
              language.},
  booktitle = \{Proceedings of TYPES 2003},
  year = \{2004}, 
  series = \{LNCS}, 
  publisher = \{Springer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/bettini.bono.likavec_core-calculus-hightorder-mixins-classes.pdf}
}

@InProceedings\{bettini.bono.likavec:core-calculus-mixinbased-incomplete-objects,
  author = \{L. Bettini and V. Bono and S. Likavec},
  title = \{A Core Calculus of Mixin-Based Incomplete Objects},
  Abstract = \{We design a calculus that combines class-based features with 
              object-based ones, with the aim of fitting into a unifying setting 
              the ``best of both worlds'. In a mixin-based approach, mixins are 
              seen as \emph{incomplete classes} from which \emph{incomplete objects} 
              can be instantiated. In turn, incomplete objects can be completed 
              in an object-based fashion. Our hybrid calculus is shown to be useful 
              in some real world scenarios that we present as examples.},
  booktitle = \{FOOL 11},
  year = \{2004}, 
  url = \{http://mikado.di.fc.ul.pt/repository/bettini.bono.likavec_core-calculus-mixinbased-incomplete-objects.pdf}
}

@InProceedings\{boreale.gorla:compositional-reasoning-spi-calculus,
  author = \{M. Boreale and D. Gorla},
  title = \{On Compositional Reasoning in the spi-calculus},
  Abstract = \{Observational equivalences can be used to reason about the
              correctness of security protocols described in the spi-calculus.
              Unlike in CCS or in pi-calculus, these equivalences do not enjoy a
              simple formulation in spi. The present paper aims at enriching the
              set of tools for reasoning on processes by providing a few equational
              laws for a sensible notion of spi-bisimilarity. We discuss the
              difficulties underlying compositional reasoning in spi and show that,
              in some cases and with  some care, the proposed laws can be used to 
              build compositional proofs. A selection of these laws forms the basis 
              of a proof system that we show to be sound and complete for the strong 
              version of bisimilarity.},
  booktitle = \{Proceedings of Foundations of Software Technology and Computation Structures 2002},
  year = \{2002}, 
  volume = \{2303}, 
  series = \{Lecturer notes in computer science}, 
  publisher = \{Springer Verlag}, 
  url = \{http://mikado.di.fc.ul.pt/repository/boreale.gorla_compositional-reasoning-spi-calculus.pdf}
}

@InProceedings\{boreale.gadduoci:denotational-testing-semantics-coinductive,
  author = \{M. Boreale and F. Gadduoci},
  title = \{Denotational Testing Semantics in Coinductive Form},
  Abstract = \{Building on recent work by Rutten on coinduction and formal power
              series, we define a denotational semantics for the {\sc csp}
              calculus and prove it fully abstract for testing equivalence.  The
              proposed methodology allows for abstract definition of operators
              in terms of {\em behavioural differential equations} and for
              coinductive reasoning on them, additionally dispensing with
              continuous order-theoretic structures.},
  booktitle = \{Proc. of MFCS 2003},
  year = \{2003}, 
  volume = \{2747}, 
  series = \{LNCS}, 
  publisher = \{Springer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/boreale.gadduoci_denotational-testing-semantics-coinductive.ps}
}

@InProceedings\{boreale.buscemi:symbolic-analysis-crypto-protocols,
  author = \{M. Boreale and M. Buscemi},
  title = \{Symbolic analysis of crypto-protocols based on modular exponentiation},
  Abstract = \{Automatic methods developed so far for analysis of security protocols
              only model a limited set of cryptographic primitives (often, only
              encryption and concatenation) and abstract from low-level features of
              cryptographic algorithms. This paper is an attempt towards closing this
              gap. We propose a symbolic technique and a decision method for analysis
              of protocols based on modular exponentiation, such as Diffie-Hellman key
              exchange. We introduce a protocol description language along with its
              semantics. Then, we propose a notion of symbolic execution and, based on
              it, a verification method. We prove that the method is sound and
              complete with  respect to the language semantics.},
  booktitle = \{Proc. of MFCS 2003},
  year = \{2003}, 
  volume = \{2747}, 
  series = \{Lecture Notes in Computer Science}, 
  publisher = \{Springer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/boreale.buscemi_symbolic-analysis-crypto-protocols.pdf}
}

@InProceedings\{boreale.buscemi.montanari:d-fusion-calculus,
  author = \{M. Boreale and M. Buscemi and U. Montanari},
  title = \{D-Fusion: a Distinctive Fusion Calculus},
  Abstract = \{We study the relative expressive power of Fusion and pi-calculus. 
              Fusion is commonly regarded as a generalisation of pi-calculus. 
              Actually, we prove that there is no uniform fully abstract 
              embedding of pi-calculus into Fusion. This fact motivates the 
              introduction of a new calculus, D-Fusion, with two binders, l 
              and n. We show that DFusion is strictly more expressive than 
              both pi-calculus and Fusion. The expressiveness gap is further 
              clarified by the existence of a fully abstract encoding of 
              mixed guarded choice into the choice-free fragment of D-Fusion.},
  booktitle = \{Proc. of APLAS04},
  year = \{2004}, 
  volume = \{3302}, 
  series = \{LNCS}, 
  publisher = \{Springer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/boreale.buscemi.montanari_d-fusion-calculus.pdf}
}

@InProceedings\{boreale.buscemi:symbolic-analysis-security-protocols,
  author = \{M. Boreale and M.G. Buscemi},
  title = \{A Method for Symbolic Analysis of Security Protocols},
  Abstract = \{In security protocols, message exchange between the intruder and 
              honest participants induces a form of state explosion which 
              makes protocol models infinite. We propose a general method for 
              automatic analysis of security protocols based on the notion of 
              frame, essentially a rewrite system plus a set of distinguished 
              terms called messages. Frames are intended to model generic 
              cryptosystems. Based on frames, we introduce a process language 
              akin to Abadi and Fournet’s applied pi. For this language, we 
              define a symbolic operational semantics that relies on 
              unification and provides finite and effective protocol models. 
              Next, we give a method to carry out trace analysis directly on 
              the symbolic model. We spell out a regularity condition on the 
              underlying frame, which guarantees completeness of our method 
              for the considered class of properties, including secrecy and 
              various forms of authentication.We show how to instantiate our 
              method to some of the most common crypto-systems, including 
              shared- and public-key encryption, hashing and Diffie-Hellman 
              key exchange.},
  booktitle = \{Theoretical Computer Science},
  year = \{To appear}, 
  url = \{http://mikado.di.fc.ul.pt/repository/boreale.buscemi_symbolic-analysis-security-protocols.pdf}
}

@InProceedings\{boreale.buscemi.montanari:general-name-binding-mechanism,
  author = \{M. Boreale and M.G. Buscemi and U. Montanari},
  title = \{A general name binding mechanism},
  Abstract = \{We study fusion and binding mechanisms in name passing process 
              calculi. To this purpose, we introduce the U-Calculus, a process 
              calculus with no I/O polarities and a unique form of binding. 
              The latter can be used both to control the scope of fusions and 
              to handle new name generation. This is achieved by means of a 
              simple form of typing: each bound name x is annotated with a set 
              of exceptions, that is names that cannot be fused to x. The new 
              calculus is proven to be more expressive than pi-calculus and 
              Fusion calculus separately. In U-Calculus, the syntactic nesting 
              of name binders has a semantic meaning, which cannot be overcome 
              by the ordering of name extrusions at runtime. Thanks to this 
              mixture of static and dynamic ordering of names, U-Calculus 
              admits a form of labelled bisimulation which is a congruence. 
              This property yields a substantial improvement with respect to 
              previous proposals by the same authors aimed at unifying the 
              above two languages. The additional expressiveness of U-Calculus 
              is also explored by providing a uniform encoding of mixed 
              guarded choice into the choice-free sub-calculus.},
  booktitle = \{Proceedings of Trustworthy Global Computing 2005 (TGC05)},
  year = \{2005}, 
  series = \{LNCS}, 
  publisher = \{Springer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/boreale.buscemi.montanari_general-name-binding-mechanism.pdf}
}

@InProceedings\{coppo.etal:mobility-types-ambients,
  author = \{M. Coppo and  M. {Dezani-Ciancaglini} and E. Giovannetti and I. Salvo},
  title = \{{\bf M}$^3$: Mobility Types for Mobile Processes in Mobile Ambients},
  Abstract = \{We present an ambient calculus in which the open capability is 
              dropped, and a new form of ``lightweight' process mobility is 
              introduced. The calculus comes equipped with a type system that 
              allows access and mobility properties to be cntrolled, along with
              the kind of values exchanged in communication. A type inference 
              procedure determines the ``minimal' requirements needed for 
              accepting a system or a component as well typed. This gives a kind 
              of principal typing. As an expressiveness test, we show that some 
              well known calculi of concurrency and mobility can be encoded in 
              our calculus in a natural way.},
  booktitle = \{CATS 2003},
  year = \{2003}, 
  volume = \{78}, 
  series = \{ENTCS}, 
  url = \{http://mikado.di.fc.ul.pt/repository/coppo.etal_mobility-types-ambients.pdf}
}

@InProceedings\{coppo.dezani-ciancaglini:fully-abstract-model,
  author = \{M. Coppo and M. {Dezani-Ciancaglini}},
  title = \{A Fully Abstract Model for Higher-Order Mobile Ambients},
  Abstract = \{Aim of this paper is to develop a filter model for a calculus with 
              mobility and higher-order value passing. We will define it for an extension
              of the Ambient Calculus in which processes can be passed as values. This 
              model turns out to be fully abstract with respect to the notion of contextual 
              equivalence where the observables are ambients at top level.},
  booktitle = \{VMCAI 2002},
  year = \{2002}, 
  pages = \{255--271}, 
  volume = \{2294}, 
  publisher = \{Springer-Verlag}, 
  url = \{http://mikado.di.fc.ul.pt/repository/coppo.dezani-ciancaglini_fully-abstract-model.pdf}
}

@InProceedings\{coppo.etal:dynamic-local-typing-mobile-ambients,
  author = \{M. Coppo and M. {Dezani-Ciancaglini} and E. Giovannetti and R. Pugliese},
  title = \{Dynamic and Local Typing for Mobile Ambients},
  Abstract = \{An ambient calculus with both static and dynamic types is presented, 
              where the latter ones represent mobility and access rights that 
              may be dynamically consumed and acquired in a controlled way. 
              Novel constructs and operations are provided to this end. 
              Type-checking is purely local, except for a global hierarchy 
              that establishes which locations have the authority to grant 
              rights to which: there is no global environment (for closed 
              terms) assigning types to names. Each ambient or process move is 
              subject to a double authorization, one static and the other 
              dynamic: static type-checking controls (communication and) 
              ``active'' mobility rights, i.e., where a given ambient or 
              process has the right to go; dynamic type-checking controls
              ``passive'' rights, i.e., which ambients a given ambient may be 
              crossed by and which processes it may receive.},
  booktitle = \{TCS '04},
  year = \{2004}, 
  pages = \{583--596}, 
  publisher = \{Kluwer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/coppo.etal_dynamic-local-typing-mobile-ambients.pdf}
}

@InProceedings\{lacoste:building-reliable-infrastructures,
  author = \{M. Lacoste},
  title = \{Building Reliable Distributed Infrastructures Revisited: a Case Study},
  Abstract = \{Building reliable distributed infrastructures still remains a 
              challenge. Two separate and slowly diverging visions for solutions 
              have emerged: the first relies upon an implementation-based approach 
              of today's now mature middleware object technologies, often without 
              much concern for the underlying theoretical foundations. The second 
              focuses on elaborate theoretical models of distributed computation, 
              to capture various aspects of communication, mobility, or security, 
              but has produced few implementations. We attempt to reconcile on a
              case study those two opposite views of reliable distributed computing
              using a simple methodology: define both a carefully designed distributed 
              computing model with a well-defined semantics and a middleware 
              implementation that strictly conforms to the model. We demonstrate the 
              feasibility and the soundness of such a formal approach by describing 
              the refinement steps in the formalization, from the model design to the 
              implementation, using as an example a simple distributed programming model 
              named DCP. In DCP, remote interaction is primitive and the distribution of
              resources is explicit while keeping network communications transparent to 
              the programmer. The DCP implementation is formalized by a distributed
              abstract machine, and seamlessly integrated with a middleware representative 
              of current distributed technology -- the Jonathan Object Request Broker -- 
              to support network transparent communications.},
  booktitle = \{International DOA Workshop on Foundations of Middleware Technologies (WFoMT'02)},
  year = \{2002}, 
  url = \{http://mikado.di.fc.ul.pt/repository/lacoste_building-reliable-infrastructures.pdf}
}

@InProceedings\{bidinger.stefani:the-kell-calculus,
  author = \{P. Bidinger and J.B. Stefani},
  title = \{The Kell calculus: operational semantics and type system},
  Abstract = \{This paper presents the Kell calculus, a new distributed process 
              calculus that retains the original insights of the Seal calculus (local
              actions, process replication) and of the M-calculus (higher-order processes
              and programmable membranes), although in a much simpler setting than the 
              latter. The calculus is equipped with a type system that enforces a unicity 
              property for location names that is crucial for the efficient implementation 
              of the calculus.},
  booktitle = \{Proceedings 6th IFIP International Conference on Formal Methods for Open 
                 Object-based Distributed Systems (FMOODS 03)},
  year = \{2003}, 
  volume = \{2884}, 
  series = \{LNCS}, 
  publisher = \{Springer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/bidinger.stefani_the-kell-calculus.ps}
}

@InProceedings\{chadha.kremer.scedrov:multi-party-contract-signing,
  author = \{R. Chadha and S. Kremer and A. Scedrov},
  title = \{Formal analysis of multi-party contract signing},
  Abstract = \{We analyze the multi-party contract-signing protocols of Garay
              and MacKenzie (GM) and of Baum and Waidner (BW). We use a finite-state
              tool, Mocha, which allows specification of protocol properties in a
              branching-time temporal logic with game semantics. While our analysis
              does not reveal any errors in the BW protocol, in the GM protocol we
              discover serious problems with fairness for four signers and an
              oversight regarding abuse-freeness for three signers. We propose a
              complete revision of the GM subprotocols in order to restore fairness.},
  booktitle = \{Workshop on Issues in the Theory of Security---WITS 04},
  year = \{2004}, 
  url = \{http://mikado.di.fc.ul.pt/repository/chadha.kremer.scedrov_multi-party-contract-signing.ps}
}

@InProceedings\{nicola.etal:global-computing-dynamic-network,
  author = \{R. {De Nicola} and D. Gorla and R. Pugliese},
  title = \{Global Computing in a Dynamic Network of Tuple Spaces},
  Abstract = \{We present a calculus inspired by Klaim whose main features are: 
              explicit process distribution and node interconnections, remote 
              operations, process mobility and asynchronous communication 
              through distributed tuple spaces. We first introduce a basic 
              language where connections are reliable and immutable; then, we 
              enrich it with two more advanced features for global computing, 
              i.e. failures and dynamically evolving connections. In each 
              setting, we use our formalisms to specify some non-trivial 
              global computing applications and exploit the semantic theory 
              based on an observational equivalence to equationally establish
              properties of the considered case-studies.},
  booktitle = \{Proc. of 7th International Conference on Coordination Models and Languages (COORDINATION 2005)},
  year = \{2005}, 
  pages = \{157--172}, 
  volume = \{3454}, 
  series = \{LNCS}, 
  publisher = \{Springer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/nicola.etal_global-computing-dynamic-network.pdf}
}

@InProceedings\{nicola.gorla.pugliese:expressive-power-klaim-based-calculi,
  author = \{R. {De Nicola} and D. Gorla and R. Pugliese},
  title = \{On the Expressive Power of KLAIM-based Calculi},
  Abstract = \{In this work, we study the expressive power of variants of KLAIM,
	      an experimental language with programming primitives for global
	      computing that combines the process algebra approach with the
	      coordination-oriented one. KLAIM has proved to be suitable for
	      programming a wide range of distributed applications with agents
	      and code mobility, and has been implemented on the top of a
	      runtime system based on Java. The expressivity of its constructs
	      is tested by distilling from it some (more and more foundational)
	      calculi and studying the encoding of each of the considered
	      languages into a simpler one. An encoding of the asynchronous pi-calculus
	      into one of these calculi is also presented.},
  booktitle = \{Proceedings of 11th International Workshop on Expressiveness in Concurrency (EXPRESS'04)},
  year = \{2004}, 
  series = \{ENTCS}, 
  publisher = \{Elsevier}, 
  url = \{http://mikado.di.fc.ul.pt/repository/nicola.gorla.pugliese_expressive-power-klaim-based-calculi.pdf}
}

@InProceedings\{de-nicola.etal:formal-reasoning-programmable-qos,
  author = \{R.~{De Nicola} and G.-L.~Ferrari and U.~Montanari and R.~Pugliese and E.~Tuosto},
  title = \{A Formal Basis for Reasoning on Programmable QoS},
  Abstract = \{The explicit management of Quality of Service (QoS) of network
              connectivity, such as, e.g., working cost, transaction support, and security,
              is a key requirement for the development of the novel wide area network
              applications. In this paper, we introduce a foundational model for specification
              of QoS attributes at application level. The model handles QoS attributes as semantic
              constraints within a graphical calculus for mobility. In our approach QoS attributes
              are related to the programming abstractions and are exploited to select, configure
              and dynamically modify the underlying system oriented QoS mechanisms.},
  booktitle = \{International Symposium on Verification (Theory and Practice)--Celebrating Zohar Manna's 64-th Birthday},
  year = \{2003}, 
  volume = \{2772}, 
  series = \{LNCS}, 
  publisher = \{Springer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/de-nicola.etal_formal-reasoning-programmable-qos.pdf}
}

@InProceedings\{epardaud:mobile-reactive-programming-uml,
  author = \{S. Epardaud},
  title = \{Mobile reactive programming in ULM},
  Abstract = \{We present an embedding of ULM in Scheme and an implementation of 
              a compiler and a 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.},
  booktitle = \{Scheme Workshop},
  year = \{2004}, 
  url = \{http://mikado.di.fc.ul.pt/repository/epardaud_mobile-reactive-programming-uml.pdf}
}

@InProceedings\{vasconcelos.etal:session-types-functional-multithreading,
  author = \{V. Vasconcelos and A. Ravara and S. Gay},
  title = \{Session types for functional multithreading},
  Abstract = \{We define a language whose type system, incorporating session types, 
              allows complex protocols to be specified by types and verified 
              by static typechecking. A session type, associated with a 
              communication channel, specifies the state transitions of a 
              protocol and also the data types of messages associated with 
              transitions; thus typechecking can verify both correctness of 
              individual messages and correctness of sequences of transitions.
              Previously session types have mainly been studied in the context 
              of the pi-calculus; instead, our formulation is based on a 
              multi-threaded functional language with side-effecting 
              input/output operations. Our typing judgements statically 
              describe dynamic changes in the types of channels, our channel 
              types statically track aliasing, and our function types not only
              specify argument and result types but also describe changes in 
              channels. We formalize the syntax, semantics and typing system 
              of our language, and prove subject reduction and runtime type 
              safety theorems. We also present a type checking algorithm and 
              show that it is correct with respect to the type system.},
  booktitle = \{CONCUR '04},
  year = \{2004}, 
  pages = \{497--511}, 
  volume = \{3170}, 
  series = \{LNCS}, 
  publisher = \{SPRINGER}, 
  url = \{http://mikado.di.fc.ul.pt/repository/vasconcelos.etal_session-types-functional-multithreading.pdf}
}

------------------
- TechReport  -
------------------

@TechReport\{jeffrey.rathke:contextual-equivalence,
  author = \{A. Jeffrey and J. Rathke},
  title = \{Contextual equivalence for higher-order pi-calculus revisited},
  Abstract = \{The higher-order pi-calculus is an extension of the pi-calculus to 
              allow communication of abstractions of processes rather than names 
              alone. It has been studied intensively by Sangiorgi in his thesis 
              where a characterisation of a contextual equivalence for higher-order 
              pi-calculus is provided using labelled transition systems and normal 
              bisimulations. Unfortunately the proof technique used there requires
              a restriction of the language to only allow finite types. We revisit 
              this calculus and offer an alternative presentation of the labelled
              transition system and a novel proof technique which allows us to
              provide a fully abstract characterisation of contextual equivalence
              using labelled transitions and bisimulations for higher-order
              pi-calculus with recursive types also.},
  institution = \{{COGS},University of Sussex},
  year = \{2002}, 
  number = \{2002:04}, 
  url = \{http://mikado.di.fc.ul.pt/repository/jeffrey.rathke_contextual-equivalence.pdf}
}

@TechReport\{ravara.etal:lsdpi-report,
  author = \{A. Ravara and A. Matos and V. Vasconcelos and L. Lopes},
  title = \{A lexically scoped distributed pi-calculus},
  Abstract = \{We define the syntax, the operational semantics, and a type system 
              for lsdpi, an asynchronous and distributed pi-calculus with local 
              communication and process migration. The calculus follows a simple
              model of distribution for mobile calculi, with a lexical scoping 
              mechanism that provides for both remote communication and process
              migration, and makes explicit migration primitives superfluous.},
  institution = \{DIFCUL},
  year = \{2002}, 
  type = \{DI/FCUL TR}, 
  number = \{02--4}, 
  url = \{http://mikado.di.fc.ul.pt/repository/ravara.etal_lsdpi-report.pdf}
}

@TechReport\{martins.vasconcelos:controlling-security-policies,
  author = \{F. Martins and V. Vasconcelos},
  title = \{Controlling Security Policies in a Distributed Environment},
  Abstract = \{This paper presents a type system to control the migration of code 
              between nodes in a concurrent distributed framework, using Dpi. 
              We express resource policies with types and enforce them via a 
              type system. Sites are organised hierarchically in subnetworks 
              that share the same security policies, statically specified by 
              a network administrator. The type system guarantees that, at 
              runtime, there are no security policies violations.},
  institution = \{Department of Computer Science, University of Lisbon},
  year = \{2004}, 
  type = \{DI/FCUL TR}, 
  number = \{04--01}, 
  url = \{http://mikado.di.fc.ul.pt/repository/martins.vasconcelos_controlling-security-policies.pdf}
}

@TechReport\{higher-order-distributed-components,
  author = \{J.B. Stefani},
  title = \{A Calculus of Higher-Order Distributd Components},
  Abstract = \{This report presents a calculus for higher-order distributed
              components, the Kell calculus.  The calculus can be understood as a
              direct extension of the higher-order $pi$-calculus with programmable
              locations. The report illustrates the expressive power of the Kell
              calculus by encoding several process calculi with explicit locations,
              including Mobile Ambients, the Distributed Join calculus and the
              {mcalc}. The latter encoding demonstrates that the Kell calculus
              retains the expressive power of the {mcalc} but in a much simpler
              setting.},
  institution = \{INRIA},
  year = \{2003}, 
  number = \{RR-4692}, 
  url = \{http://mikado.di.fc.ul.pt/repository/higher-order-distributed-components.pdf}
}

@TechReport\{hennessy.rathke.yoshida:safedpi,
  author = \{M. Hennessy and J. Rathke and N. Yoshida},
  title = \{SafeDpi: a language for controlling mobile code},
  Abstract = \{SafeDpi is a distributed version of the picalculus, in
              which processes are located at dynamically created sites.
              Parametrised code may be sent between sites using so-called ports,
              which are essentially higher-order versions of picalculus 
              communication channels. A host location may protect itself
              by only accepting code which conforms to a given type associated
              to the incoming port.

              We define a sophisticated static type system for these ports, which
              restrict the capabilities and access rights of any processes launched
              by incoming code. Dependent and existential types are used to add
              flexibility, allowing the behaviour of these launched processes,
              encoded as process types, to depend on the host's instantiation
              of the incoming code.
              We also show that a natural contextually defined behavioural
              equivalence can be characterised coinductively, using bisimulations
              based on typed actions. The characterisation is based on the
              idea of knowledge acquisition by a testing environment and makes
              explicit some of the subtleties of determining equivalence in this
              language of highly constrained distributed code.},
  institution = \{University of Sussex},
  year = \{2003}, 
  number = \{2003:02}, 
  url = \{http://mikado.di.fc.ul.pt/repository/hennessy.rathke.yoshida_safedpi.pdf}
}

@TechReport\{hennessy.merro.rathke:towards-behavioural-theory,
  author = \{M. Hennessy and M. Merro and J. Rathke},
  title = \{Towards a behavioural theory of access and mobility control in distributed systems},
  Abstract = \{We define a typed bisimulation equivalence for the language Dpi, a
              distributed version of the pi-calculus in which processes may migrate
              between dynamically created locations. It takes into account resource
              access policies, which can be implemented in Dpi using a novel form of
              dynamic capability types. The equivalence, based on typed actions between
              configurations, is justified by showing that it is fully-abstract with
              respect to a natural distributed version of a contextual equivalence. In
              the second part of the paper we study the effect of controlling the
              migration of processes. This affects the ability to perform observations
              at specific locations, as the observer may be denied access. We show how
              the typed actions can be modified to take this into account, and generalise
              the full-abstraction result to this more delicate scenario.},
  institution = \{{COGS},University of Sussex},
  year = \{2002}, 
  number = \{2002:01}, 
  url = \{http://mikado.di.fc.ul.pt/repository/hennessy.merro.rathke_towards-behavioural-theory.pdf}
}

@TechReport\{lacoste:survey-implementation-membranes,
  author = \{M. Lacoste},
  title = \{A Survey of Some Implementation Techniques for Security Membranes},
  Abstract = \{The notion of security membrane appears as an emerging concept in the 
              design of secure languages for global computing. Membranes separate 
              the computational behavior of a site from the security code 
              controlling access to site-located resources. We provide a survey of 
              some of the challenges which arise when trying to implement security 
              membranes in an execution platform such as an operating system. We 
              identify four main design issues: the choice of a security model; the 
              type of architecture for the execution environment; the layer at which 
              to place security mechanisms; and the assurance level of the platform. 
              In each case, we discuss possible trade-offs between security, 
              flexibility, simplicity, and trustworthiness. We then show how 
              applying a component-based approach to design and implement the 
              execution environment can help to reach an acceptable compromise 
              between such properties.},
  institution = \{France Telecom R&D},
  year = \{2004}, 
  url = \{http://mikado.di.fc.ul.pt/repository/lacoste_survey-implementation-membranes.pdf}
}

@TechReport\{lacoste:imc-flexible-communication-support,
  author = \{M. Lacoste},
  title = \{IMC: Flexible Communication Support for Implementing Mobile Process Calculi},
  Abstract = \{Existing implementations of distributed process calculi
              exhibit a wide diversity of communication protocols and interaction 
              semantics between locations. Thus, a core framework, such as IMC 
              (Implementing Mobile Calculi), aiming to provide the programmer with 
              a toolbox to build implementations of new process calculi, should be 
              flexible enough to support multiple marshalling strategies, while being
              minimal to enable an easy introduction of new communication protocols. 
              In this paper, we report on the IMC Protocol Management Framework, a
              Java class library which allows to define customized protocol stacks
              by composing micro-protocols in a flexible manner. We describe in detail
              both its interfaces and mechanisms, focusing on the TCP/IP layer, which 
              constitutes the network interface of most protocols stacks used in 
              existing process calculi implementations. In particular, we illustrate 
              how new protocols can be introduced with IMC, by showing the protocol 
              and session objects involved, and by describing the path followed by 
              messages within a protocol stack.},
  institution = \{France Telecom R.D.},
  year = \{2003}, 
  url = \{http://mikado.di.fc.ul.pt/repository/lacoste_imc-flexible-communication-support.ps}
}

@TechReport\{lacoste:phd-thesis,
  author = \{M. Lacoste},
  title = \{A Distributed Virtual Machine for Programming Mobile Processes},
  Abstract = \{Building reliable distributed infrastructures for programming
              on wide-area networks is hampered by: a lack of reference point for
              programming constructs; and a divergence between principles and 
              practice of distributed programming. This dissertation investigates
              the notion of domain as a possible founding abstraction for global
              computing. A domain offers a uniform view of partitions occuring in
              large distributed systems. We show the notion of domain is directly
              implementable, using a simple methodology to build reliable domain-based
              infrastructures. Formalization consists in the following refinement 
              steps: formal model of distributed computation > formal specification 
              > implementation. We apply this methodology to a domain-based model of 
              distributed computation, the M-calculus: we define a distributed
              abstract machine and a virtual machine for the M-calculus. A qualitative 
              evaluation shows the effectiveness of the proposed approach to building
              reliable distributed infrastructures.},
  institution = \{France Telecom R.D.},
  year = \{2003}, 
  number = \{NT/FTR.D./8308}, 
  url = \{http://mikado.di.fc.ul.pt/repository/lacoste_phd-thesis.ps.gz}
}

@TechReport\{nicola.gorla.pugliese:basic-observables-calculus-gc,
  author = \{R. {De Nicola} and D. Gorla and R. Pugliese},
  title = \{Basic Observables for a Calculus for Global Computing},
  Abstract = \{We discuss a basic process calculus useful for modelling
	      applications over global computing systems and present the
	      associated semantic theories as determined by some basic notions
	      of observation. The main features of the calculus are explicit
	      distribution, remote operations, process mobility and asynchronous
	      communication through distributed data spaces. We introduce some
	      natural notions of extensional observations and study their
	      closure under operational reductions and/or language contexts to
	      obtain barbed congruence and may testing. For these
	      equivalences, we provide alternative tractable characterizations
	      as labelled bisimulation and trace equivalence. We discuss some of
	      the induced equational laws and relate them to design choices of
	      the calculus. In particular, we show that some of these laws do
	      not hold any longer if the language is rendered less abstract by
	      introducing (asynchronous and undetectable) failures or by
	      implementing remote communications via process migrations and
	      local exchanges. In both cases, we also investigate the adaptation
	      of the tractable characterizations of barbed congruence and may
	      testing to the lower-level scenarios.},
  institution = \{Dip. di Informatica, Univ. di Roma ``La Sapienza"},
  year = \{2004}, 
  number = \{07/2004}, 
  url = \{http://mikado.di.fc.ul.pt/repository/nicola.gorla.pugliese_basic-observables-calculus-gc.pdf}
}

@TechReport\{gay.vasconcelos.ravara:session-types,
  author = \{S. Gay and V. Vasconcelos and A. Ravara},
  title = \{Session Types for Inter-Process Communication},
  Abstract = \{We define a language whose type system, incorporating session types,
              allows complex protocols to be specified by types and verified by
              static typechecking. A session type, associated with a
              communication channel, specifies not only the data types of
              individual messages, but also the state transitions of a protocol
              and hence the allowable sequences of messages. Although session
              types are well understood in the context of the pi-calculus, our
              formulation is based on lambda-calculus with side-effecting
              input/output operations and is different in significant ways. Our
              typing judgements statically describe dynamic changes in the types
              of channels, our channel types statically track aliasing, and our
              function types not only specify argument and result types but also
              describe changes in channel types. After formalising the syntax,
              semantics and typing rules of our language, and proving a subject
              reduction theorem, we outline some possibilities for extending
              this work to a concurrent object-oriented language.},
  institution = \{Department of Computing, University of Glasgow},
  year = \{2003}, 
  number = \{2003--133}, 
  url = \{http://mikado.di.fc.ul.pt/repository/gay.vasconcelos.ravara_session-types.pdf}
}

@TechReport\{owen.rathke.wakeman:jpolicy-Java-extension,
  author = \{T. Owen and J. Rathke and I. Wakeman},
  title = \{JPolicy: a Java extension for dynamic access control},
  Abstract = \{The development of remote execution platforms, where
              service hosts accept code from third party clients and run it on their
              behalf, provides a powerful alternative to the RPC model of clients
              invoking remote services over a network. A major concern for service
              hosts is to control access and usage of their own services and
              resources, whether the client code is being executed by the service host
              itself or operating remotely and using RPC. We introduce a set of
              extensions to Java that enables service hosts to control how their
              services may be used by client Java programs, according to a specified
              policy. We separate the policies from the services being controlled,
              rather than fixing the policy at compile-time or load-time. A novel
              aspect of this work is that the policies allow dynamic access control to
              services: the availability of service functionality can vary during
              execution. Furthermore, we support the changing of policies at run-time
              without modification to service code or clients. We describe our
              implementation of these language extensions and show how the system
              enables service providers to enforce policies that protect their
              resources and services from undesirable client code behaviour.},
  institution = \{University of Sussex},
  year = \{2004}, 
  type = \{Informatics Computer Science R}, 
  number = \{2004:01}, 
  url = \{http://mikado.di.fc.ul.pt/repository/owen.rathke.wakeman_jpolicy-Java-extension.ps}
}

-----------------
- Deliverables  -
-----------------

@Unpublished\{D4.1,
  author = \{Mikado Consortium},
  title = \{The Mikado Global Computing Project: An executive presentation},
  Abstract = \{This document presents a brief summary of the Mikado project:
              its scientific and technical objectives, its innovative aspects and expected
              results, its organization, and its partners.},
  year = \{2002}, 
  note = \{Mikado Deliverable D4.1}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D4.1.pdf}
}

@Unpublished\{D1.1.1,
  author = \{G.Boudol and I. Castellani and F. Germain and M. Lacoste},
  title = \{Analysis of formal models of distribution and mobility: state of the art.},
  Abstract = \{This document presents a comparative analysis of various models
              and languages for mobile code, incorporating some notion of site or more
              generally of domain. These models and languages will be referred to as
              distributed mobile calculi. Our study will focus on three aspects of these
              calculi: distribution, mobility and security. Moreover, it will emphasize
              the notion of domain as a primitive programming concept and illustrate its
              semantics in the various calculi.},
  year = \{2002}, 
  note = \{Mikado Deliverable D1.1.1}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D1.1.1v1.0.pdf}
}

@Unpublished\{D2.1.1,
  author = \{E. Giovannetti, M. Hennessy, J. Rathke},
  title = \{Type systems and static analysis for mobile and distributed computing: state of the art},
  Abstract = \{},
  year = \{2002}, 
  note = \{Mikado Deliverable D2.1.1}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D2.1.1.pdf}
}

@Unpublished\{D3.1.1,
  author = \{M. Boreale and R. {De Nicola} and M. Lacoste and V. Vasconcelos},
  title = \{Analysis of distributed execution structures: state of the art},
  Abstract = \{The goal of this document is to give an overview of the state of 
              the art in execution structures for global programming languages. The
              introductory section touches upon the main issues that arise in connection
              with the design of global applications. Existing paradigms, technologies
              and languages for global programming are the subject of Part 1. Part 2
              analyzes in detail the execution structures of those languages that are
              central to the project.},
  year = \{2002}, 
  note = \{Mikado Deliverable D3.1.1}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D3.1.1v1.0.pdf}
}

@Unpublished\{D4.2,
  author = \{J. B. Stefani},
  title = \{Dissemination and use plan},
  Abstract = \{This document presents the Dissemination and use Plan of the Mikado
              Global Computing Project. The basis of the document is the common template
              adopted by the projects participating in the Global Computing  Analysis of
              Systems and Security  Cluster (DART, Mikado, MRG, MyTHS, Profundis, and
              Secure).},
  year = \{2002}, 
  note = \{Mikado Deliverable D4.2}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D4.2.pdf}
}

@Unpublished\{D1.1.2,
  author = \{J. B. Stefani},
  title = \{Requirements for a programming model for global computing},
  Abstract = \{This document presents a set of requirements for a global 
              computing programming model. Requirements are grouped into eight classes 
              covering issues ranging from implementability and effectiveness to support
              for high-level coordination and atomic activities abstractions.},
  year = \{2003}, 
  note = \{Mikado Deliverable D1.1.2}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D1.1.2v1.0.pdf}
}

@Unpublished\{D4.3,
  author = \{J. B. Stefani},
  title = \{Self-Evaluation Plan},
  Abstract = \{This document presents the Self-Evaluation Plan of the 
              Mikado Global Computing Project. The basis of the document is the common 
              template adopted by the projects participating in the Global Computing  
              Analysis of Systems and Security  Cluster.},
  year = \{2003}, 
  note = \{Mikado Deliverable D1.1.2}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D4.3.pdf}
}

@Unpublished\{D1.2.0,
  author = \{G. Boudol},
  title = \{Core programming model, release 0},
  Abstract = \{},
  year = \{2002}, 
  note = \{Mikado Deliverable D1.2.0}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D1.2.0.pdf}
}

@Unpublished\{D2.1.0,
  author = \{D. Gorla},
  title = \{Flat Net Architectures for Global Computing Systems: Types and Behaviour},
  Abstract = \{},
  year = \{2002}, 
  note = \{Mikado Deliverable D2.1.0}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D2.1.0.pdf}
}

@Unpublished\{D3.1.0,
  author = \{L. Bettini and R. De Nicola and M. Lacoste and L. Lopes and V. Vasconcelos},
  title = \{Virtual machine technology : Core software framework, v0},
  Abstract = \{This document presents the Dissemination and use Plan of the Mikado
              Global Computing Project. The basis of the document is the common template
              adopted by the projects participating in the Global Computing  Analysis of
              Systems and Security  Cluster (DART, Mikado, MRG, MyTHS, Profundis, and
              Secure).},
  year = \{2002}, 
  note = \{Mikado Deliverable D3.1.0}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D3.1.0v1.0.pdf}
}

@Unpublished\{D4.4,
  author = \{G. Boudol and M. Hennessy and M. Lacoste and R. de Nicola and J. B. Stefani and V. Vasconcelos},
  title = \{Annual project report Year 1},
  Abstract = \{},
  year = \{2002}, 
  note = \{Mikado Deliverable D4.4}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D4.4_D4.5.pdf}
}

@Unpublished\{D4.5,
  author = \{G. Boudol and M. Hennessy and M. Lacoste and R. de Nicola and J. B. Stefani and V. Vasconcelos},
  title = \{Dissemination and Evaluation report: Year 1},
  Abstract = \{},
  year = \{2002}, 
  note = \{Mikado Deliverable D4.5}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D4.4_D4.5.pdf}
}

@Unpublished\{D1.2.1,
  author = \{G. Boudol},
  title = \{A parametric model of migration and mobility, release 1},
  Abstract = \{},
  year = \{2003}, 
  note = \{Mikado Deliverable D1.2.1}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D1.2.1.pdf}
}

@Unpublished\{D2.1.2,
  author = \{},
  title = \{Type systems for Mikado inspired mobility and security programming concepts},
  Abstract = \{},
  year = \{2003}, 
  note = \{Mikado Deliverable D2.1.2}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D2.1.2.ps}
}

@Unpublished\{D2.2.1,
  author = \{M. Hennessy},
  title = \{Co-inductive proof techniques},
  Abstract = \{},
  year = \{2003}, 
  note = \{Mikado Deliverable D2.2.1}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D2.2.1.pdf}
}

@Unpublished\{D1.3.1,
  author = \{},
  title = \{Study of alternate distributed models, release 1},
  Abstract = \{},
  year = \{2003}, 
  note = \{Mikado Deliverable D1.3.1}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D1.3.1.pdf}
}

@Unpublished\{D2.1.3,
  author = \{},
  title = \{Resource policies expressed and checked as type systems},
  Abstract = \{},
  year = \{2003}, 
  note = \{Mikado Deliverable D2.1.3}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D2.1.3.ps}
}

@Unpublished\{D2.3.1,
  author = \{M. Loreti and R. {De Nicola} and C. Carrez and E. Najm and R. Chadha and V. Sassone},
  title = \{Modal and temporal logics for distributed behaviour},
  Abstract = \{This document presents the current results of MIKADO-related work on 
              the development and application of modal and temporal logics for 
              distributed behaviour. The main scienti contents are reported in 
              the technical annexes as the part of the deliverables, and 
              contain following documents:
              1. A modal logic for mobile agents by R. De Nicola and M. Loreti.
              2. A distributed Kripke semantics by R. Chadha, D. Macedonio and 
              V. Sassone.
              3. Bilogics: Spatial-nominal logics for bigraphs (extended 
              abstract) by G. Conforti, Macedonio and V. Sassone.
              4. Bigraphical logics for XML by G. Conforti, D. Macedonio and 
              V. Sassone.
              5. Assembling components with behavioural contracts by C. Carrez, 
              A. Fantechi, and Najm..
              6. Formal analysis of multi-party fair exchange protocols by R. 
              Chadha, S. Kremer and Scedrov},
  year = \{2003}, 
  note = \{Mikado Deliverable D2.3.1}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D2.3.1.pdf}
}

@Unpublished\{D3.1.2,
  author = \{L. Bettini and R. De Nicola and M. Lacoste and L. Lopes and V. Vasconcelos},
  title = \{Towards MIKADO Abstract Machines},
  Abstract = \{This document discusses the progress in the implementation of the
              MIKADO Core Software Frame- work, that we call IMC (Implementing
              Mobile Calculi). In particular, we describe how the four main
              components of abstract machines for mobile calculi (node topology,
              naming and binding, communication protocols and mobility) have
              been implemented. The document contains also three papers
              describing the work done by the involved sites to start
              experimenting with (part of) the core software framework.},
  year = \{2003}, 
  note = \{Mikado Deliverable D3.1.2}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D3.1.2.pdf}
}

@Unpublished\{D3.2.1,
  author = \{L. Bettini and D. Falassi and R. De Nicola and M. Loreti and M. Lacoste and L. Lopes and L. Oliveira},
  title = \{Languages experiments v1: Simple calculi as programming language},
  Abstract = \{We describe the architecture and the implementation of 
              the MIKADO software framework, that we call IMC (Implementing 
              Mobile Calculi and show how it can be used. The framework aims 
              at providing the programmer with primitives to design and 
              implement run-time systems for distributed process calculi. 
              The document describes the four main components of abstract 
              machines for mobile calculi (node topology, naming and binding, 
              communication protocols and mobility) that have been implemented
              as Java packages. The document ends with the description of three
              implementation experiments that use IMC: the re-implementation 
              of KLAVA, the run time support for KLAIM, the implementation of
              a runtime system for the Distributed Pi-Calculus and the 
              development of an instance calculus of Boudol s membrane model.},
  year = \{2003}, 
  note = \{Mikado Deliverable D3.2.1}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D3.2.1.pdf}
}

@Unpublished\{D4.6 and D4.7,
  author = \{G. Boudol and M. Hennessy and M. Lacoste and R. de Nicola and J. B. Stefani and V. Vasconcelos},
  title = \{Progress, Dissemination and Evaluation Report (Y2)},
  Abstract = \{},
  year = \{2004}, 
  note = \{MIKADO Deliverable D4.6 & D4.7}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D4.6_D4.7.pdf}
}

@Unpublished\{D2.2.2,
  author = \{D. Gorla and R. Pugliese and A. Schmitt and J.B. Stefani and A. Ciaffaglione and M. Hennessy and J.},
  title = \{Proof methodologies in a distributed setting},
  Abstract = \{This document presents the current results of Mikado-related work on 
              the development of proof methodologies applicable to formal 
              systems describing distributed behaviour. The main scientifc
              contents are reported in technical annexes, which are briefy 
              summarized below.},
  year = \{2004}, 
  note = \{Mikado Deliverable D2.2.2}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D2.2.2.pdf}
}

@Unpublished\{D1.2.2,
  author = \{F. Martins and L. Salvador and L. Lopes and V. Vasconcelos},
  title = \{An instance of the MIKADO migration model},
  Abstract = \{},
  year = \{2004}, 
  note = \{Mikado Deliverable D1.2.2}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D1.2.2.pdf}
}

@Unpublished\{D1.3.2,
  author = \{M. Coppo and R. {De Nicola]} and M. {Dezani-Ciancaglini} and E. Giovannetti and D. Gorla and D. Hirs},
  title = \{Study of Alternate Distributed Models, release 2},
  Abstract = \{},
  year = \{2004}, 
  note = \{Mikado Deliverable D1.3.2}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D1.3.2.pdf}
}

@Unpublished\{D2.1.4,
  author = \{R. {De Nicola} and D. Gorla and R. Pugliese and M. Coppo and M. Dezani and E. Giovannetti and F. Mar},
  title = \{Type systems for open networks, using the Mikado core programming models},
  Abstract = \{In the last decade, several foundational formalisms for global 
              computing have appeared in literature to improve the 
              understanding of the complex mechanisms underlying such new 
              computational scenario. In their design, the integration of 
              security mechanisms is a major challenge and great efforts have 
              been recently devoted to embed such mechanisms within standard 
              programming features. In this deliverable, we shall focus on the 
              security mechanisms put forward by type systems, that are used 
              for expressing and checking behavioural properties concerning 
              mobility, resource access, security, etc. Moreover, when dealing 
              with distributed and mobile computing in wide-area “open” 
              systems, one is often confronted with a scenario where 
              interaction may take place between parties whose respective 
              properties are unknown or only partially known to each other. If 
              stopping the execution for re-checking is to be avoided, each 
              component must dynamically carry with it sufficient behavioural 
              information that can be checked at runtime by the other ones 
              interacting with it. We present here three typing approaches 
              focussed on security properties of open systems, and on their 
              enforcement mechanisms. The solutions proposed do not rely on a 
              single process calculus but encompass three successfull models 
              for global computing systems: Dpi, Ambient and KLAIM.},
  year = \{2004}, 
  note = \{Mikado Deliverable D2.1.4}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D2.1.4.pdf}
}

@Unpublished\{D2.3.2,
  author = \{A. Francalanza and M. Hennessy and R. {De Nicola} and D. Gorla and R. Pugliese},
  title = \{System Behaviour and Reasoning in the Presence of Failure},
  Abstract = \{},
  year = \{2004}, 
  note = \{Mikado Deliverable D2.3.2}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D2.3.2.pdf}
}

@Unpublished\{D3.1.3,
  author = \{L. Bettini and R. {De Nicola} and M. Lacoste and M. Loreti},
  title = \{Virtual machine technology: Core software framework, v2},
  Abstract = \{This document discusses the progress in the implementation of the 
              MIKADO Core Software Framework, that we call IMC (Implementing 
              Mobile Calculi). The framework has been developed to build 
              run-time support for languages oriented aiming at programming 
              global computing applications. It enables platform designers to 
              customize communication protocols and network architectures and 
              guarantees transparency of name management and code mobility in 
              distributed environments. A first version of the IMC framework 
              was delivered last year [BFN+04]. The version described here has 
              been completely re-designed and implemented with the aims of 
              guaranteeing better usability and additional features. The 
              actual changes have been prompted by the actual use of the 
              framework by two units of the project. The IMC framework has 
              been used to re-engineer the KLAVA package (the runtime support 
              for KLAIM) and to implement two variants of Dpi, one of the 
              reference calculi for the mikado domain based model. 
              Investigation have started to consider the embedding the concept 
              of membrane within IMC that have lead to guidelines that will be 
              used for further implementations. The framework presented here 
              will be released as open source software. The actual code of the 
              different IMC components can be inspected at the following 
              address: http://music.dsi.unifi.it/software/},
  year = \{2004}, 
  note = \{Mikado Deliverable D3.1.3}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D3.1.3.pdf}
}

@Unpublished\{D3.2.2,
  author = \{L. Bettini and D. Falassi and R. {De Nicola} and M. Loreti and M. Lacoste and P. Bidinger and A. Sch},
  title = \{Languages experiments v2: Programming features and their implementation},
  Abstract = \{In this document, we briefly describe the main contribution to the 
              deliverable on experimenting with the implementation of most of 
              the calculi considered in the project. First, we describe how 
              two well known calculi for mobile processes KLAIM and Dpi have 
              been implemented on the top of IMC. We then describe the 
              implementation of the MiKO programming language, an instance of 
              the parametric calculus introduced in the WP1 with the TyCO 
              calculus as the content of the membrane itself. After this, we 
              outline the description of the implementation of the abstract 
              machine for an instance of the Kell Calculus that dedicates 
              particular attention to the proof of its correctness. Our 
              presentation ends with a discussion of the problem of 
              implementing security membranes on the top of an execution 
              platform.},
  year = \{2004}, 
  note = \{Mikado Deliverable D3.2.2}, 
  url = \{http://mikado.di.fc.ul.pt/repository/D3.2.2.pdf}
}

----------------
- Unpublished  -
----------------

@Unpublished\{gorla.pugliese:semantics-theory-global-computing,
  author = \{D. Gorla and R. Pugliese},
  title = \{A semantics theory for global computing systems},
  Abstract = \{We introduce cKlaim, a process calculus that can be thought of as
              a variant of the pi-calculus with process distribution, process mobility
              and asynchronous communication through distributed repositories. Upon it,
              we develop a semantic theory to reason about programs. More precisely, we
              introduce a natural contextually defined behavioural semantics, give a 
              coinductive characterization in terms of a labelled bisimulation and 
              illustrate some significant laws. Then, we smoothly tune the theory to 
              model two more concrete settings obtained by explicitly considering failures
              and node connections, two low-level features that in real life can affect 
              the underlying network infrastructure and, hence, the ability of processes 
              to perform remote operations.},
  year = \{2004}, 
  url = \{http://mikado.di.fc.ul.pt/repository/gorla.pugliese_semantics-theory-global-computing.pdf}
}

@Unpublished\{barbanera.etal:calculus-bounded-capacities,
  author = \{F. Barbanera and M. Bugliesi and M. {Dezani-Ciancaglini} and V. Sassone},
  title = \{A Calculus of Bounded Capacities},
  Abstract = \{Resource control has attracted increasing interest in foundational 
              research on distributed systems. This paper focuses on space control and
              develops an analysis of space usage in the context of an ambient-like
              calculus with bounded capacities and weighed processes, where migration
              and activation require space. A type system complements the dynamics of
              the calculus by providing static guarantees that the intended capacity
              bounds are preserved throughout the computation.},
  year = \{2003}, 
  note = \{Submitted to a journal. Extendend
                  version of cite{barbarena.etal:calculus-bounded-}, 
  url = \{http://mikado.di.fc.ul.pt/repository/barbanera.etal_calculus-bounded-capacities.pdf}
}

@Unpublished\{martins.ravara_static-control-code-migration,
  author = \{F. Martins and A. Ravara},
  title = \{Static control of code migration},
  Abstract = \{This paper presents a type system to control the migration 
              of code between sites in a concurrent distributed framework. The 
              type system constitutes a decidable mechanism to ensure specific 
              security policies, which control remote communication, process 
              migration, and channel creation. The approach is as follows: 
              each network administrator specifies sites privileges, and a 
              type system checks that the processes running at those sites, 
              as well as the composition of the sites, respect these policies.
              At runtime, well-typed networks do not violate the security 
              policies declared for each site.},
  year = \{2005}, 
  url = \{http://mikado.di.fc.ul.pt/repository/martins.ravara_static-control-code-migration.pdf}
}

@Unpublished\{martins.etal:mikado-koncurrent-objects,
  author = \{F. Martins and L. Salvador and L. Lopes and V. Vasconcelos},
  title = \{MiKO\Mikado Koncurrent Object},
  Abstract = \{MiKO is a distributed higher order instance of TyCO-calculus
	      based on the MIKADO's membrane model, distributing processes over
              a flat network of domains.
	
              The migration of code from one domain to another passes always 
              through the domains's membranes. The calculus contains special 
              primitives to handle migration between such domains.

              The paper presents the syntax, operational semantics, and type 
              system for MiKO.},
  year = \{2005}, 
  url = \{http://mikado.di.fc.ul.pt/repository/martins.etal_mikado-koncurrent-objects.pdf}
}

@Unpublished\{martins.vasconcelos:history-based-access-control,
  author = \{F. Martins and V. Vasconcelos},
  title = \{History-based access control for distributed processes},
  Abstract = \{This paper presents a type system to control the migration of code 
              between network nodes in a concurrent distributed framework, using 
              the Dpi language. We express resource access policies as types and
              enforce policies via a type system. Types describe paths travelled
              by migrating code, enabling the control of history sensitive access
              to resources. Sites are logically organised in subnetworks that share
              the same security policies, statically specified by a network
              administrator. The type system guarantees that well-typed networks 
              are exempt from security policies violations at runtime.},
  year = \{2005}, 
  url = \{http://mikado.di.fc.ul.pt/repository/martins.vasconcelos_history-based-access-control.pdf}
}

@Unpublished\{coppo.ciancaglini.giovannetti:the-m3-paradigm,
  author = \{M. Coppo and  M. {Dezani-Ciancaglini} and E. Giovannetti},
  title = \{The M3 Paradigm: Types and Type Inference for Ambient and Process Mobility},
  Abstract = \{A new kind of ambient calculi is presented, wherethe open
              capability is replaced by direct mobility of naked processes, while the
              associated type systems are algorithmic in the sense that they directly
              provide type inference procedures. The calculus comes equipped with a
              labelled transition system in which types play a major role: this system
              allows us to showinteresting algebraic lows. Types express, as usual, the
              communication, access and mobilityproperties of the modelled system;
              inferred types express the minimal constraints required for the system to
              well behave.},
  year = \{2004}, 
  note = \{Submitted to a journal. Extendend
                  version of \cite{coppo.etal:mobility-types-ambie}, 
  url = \{http://mikado.di.fc.ul.pt/repository/coppo.ciancaglini.giovannetti_the-m3-paradigm.pdf}
}

@Unpublished\{de-nicola.loreti:open-nets-contexts-properties,
  author = \{R. {De Nicola} and M. Loreti},
  title = \{Open Nets Contexts and Their Properties},
  Abstract = \{KLAIM (A Kernel Language for Agents an Mobility) is a simple
              formalism that can be used to model and program mobile systems; it
              allows programmers to concentrate on the distributed structure of
              programs while ignoring their precise physical allocations. For
              establishing properties of KLAIM Nets, a logic based on HML was
              defined. This logic permits specifying properties related to
              resource allocation, security and behaviours. A weakness of the
              approach is that, in order to use KLAIM and its associated logic
              to establish nets properties one needs to have a full implementation
              of the system under consideration. This is a very strong assumption
              when dealing with wide area networks, because very often, only a
              fragment of the system is known and a limited knowledge of the
              overall context is available. In the paper, after recalling KLAIM
              and its logic, we shall present a framework for specifying contexts
              for KLAIM. Then, by relying on a notion of agreement, we shall set
              up a framework ensuring that, whenever an abstract specification
              is partially implemented as a concrete net (guaranteeing agreement
              with specifications) all formulae satisfied by the more abstract
              description are satisfied also by the refined one.},
  year = \{2004}, 
  note = \{submitted}, 
  url = \{http://mikado.di.fc.ul.pt/repository/de-nicola.loreti_open-nets-contexts-properties.pdf}
}

@Unpublished\{guan:ambients-routing-calculus,
  author = \{X. Guan},
  title = \{From Ambients to a routing calculus},
  Abstract = \{From a more simplified encoding of $pi$-calculus into pure ambients,
              we derive a routing calculus which is simple and expressive. While
              being a direct subset of pure robust ambients, the basic version
              of this calculus is able to encode $pi$, and simulate D$pi$ to
              some extent. By adding a primitive that enables mobile agent
              acquiring the current location name, the calculus is able to give
              a reasonable and much simpler encoding of D$pi$.},
  year = \{2003}, 
  url = \{http://mikado.di.fc.ul.pt/repository/guan_ambients-routing-calculus.pdf}
}