%%% Please DO NOT EDIT this file - it was automatically generated.
%%% Publications of the PROFUNDIS project, EU FET-GC contract IST-2001-33100
%%%
%%% ====================================================================
%%%  BibTeX-file{
%%%     author          = "Bj{\"o}rn Victor",
%%%     date            = "06 Apr 2005",
%%%     filename        = "profundis-year3-bib.bib",
%%%     url             = "http://www.it.uu.se/profundis/profundis-year3-bib.bib",
%%%     www-home        = "http://www.it.uu.se/profundis/",
%%%     address         = "Department of Information Technology,
%%%                        Uppsala University,
%%%                        Box 337,
%%%                        SE-751 05 Uppsala, SWEDEN",
%%%     telephone       = "+46 18 471 0000",
%%%     FAX             = "+46 18 511925",
%%%     email           = "Bjorn.Victor at it.uu.se",
%%%     dates           = {2002--},
%%%     keywords        = "",
%%%     supported       = "yes",
%%%     supported-by    = "Bj{\"o}rn Victor",
%%%     abstract        = "Publications of the PROFUNDIS project,
%%%			   EU FET-GC contract IST-2001-33100"
%%%  }
%%% ====================================================================

@STRING{lncs	= "Lecture Notes in Computer Science" }
@STRING{springer= "Springer Verlag" }

@InProceedings{	  amadio.rm.dal-zilio.s:resource-control-for-synchronous-cooperative-threads,
  author	= {Amadio, Roberto M. and {Dal Zilio}, Silvano},
  title		= {{Resource Control for Synchronous Cooperative Threads}},
  booktitle	= {CONCUR 2004 -- 15th International Conference on
		  Concurrency Theory},
  series	= {Lecture Notes in Computer Science},
  volume	= {3170},
  publisher	= {Springer-Verlag},
  pages		= {68--82},
  month		= aug,
  year		= 2004
}

@InProceedings{	  baldamus.m.bengtson.j.ea:web,
  author	= {Michael Baldamus and Jesper Bengtson and Gianluigi Ferrari
		  and Roberto Raggi},
  title		= {Web Services as a New Approach to Distributing and
		  Coordinating Semantics-Based Verification Toolkits},
  booktitle	= {Proceedings of the First International Workshop on Web
		  Services and Formal Methods (WSFM 2004)},
  pages		= {11-20},
  year		= 2004,
  volume	= 105,
  series	= {ENTCS},
  month		= feb,
  publisher	= {Elsevier}
}

@InProceedings{	  baldamus.m.parrow.j.ea:spi,
  author	= {Michael Baldamus and Joachim Parrow and Bj{\"o}rn Victor},
  title		= {Spi Calculus Translated to pi-Calculus Preserving
		  May-Tests},
  booktitle	= {Proceedings of LICS'04},
  year		= 2004,
  month		= jul,
  address	= {Turku, Finland},
  organization	= {IEEE},
  publisher	= "Computer Society Press",
  abstract	= {We present a concise and natural encoding of the
		  spi-calculus into the more basic $\pi$-calculus and
		  establish its correctness with respect to a formal notion
		  of testing. This is particularly relevant for security
		  protocols modelled in spi since the tests can be viewed as
		  adversaries. The translation has been implemented in a
		  prototype tool. As a consequence, protocols can be
		  described in the spi calculus and analysed with the
		  emerging flora of tools already available for $\pi$. The
		  translation also entails a more detailed operational
		  understanding of spi since high level constructs like
		  encryption are encoded in a well known lower level. The
		  formal correctness proof is nontrivial and interesting in
		  its own; so called context bisimulations and new techniques
		  for compositionality make the proof simpler and more
		  concise. }
}

@InProceedings{	  baldi.g.bracciali.a.ea:a-coordination-based-methodology-for-security-protocol-verification,
  author	= {Baldi, Giacomo and Bracciali, Andrea and Ferrari,
		  Gianluigi and Tuosto, Emilio},
  title		= {{A Coordination-based Methodology for Security Protocol
		  Verification}},
  booktitle	= {WISP'04},
  year		= {2005},
  series	= {ENCTS},
  publisher	= {Elsevier},
  volume	= {121}
}

@Article{	  barthe.g.basu.a.ea:security,
  author	= {G. Barthe and A. Basu and T. Rezk},
  title		= {Security Types Preserving Compilation},
  year		= {2005},
  journal	= {Journal of Computer Languages, Systems and Structures},
  note		= {To appear},
  abstract	= {Starting from the seminal work of Volpano and Smith, there
		  has been growing evidence that type systems may be used to
		  enforce confidentiality of programs through
		  non-interference. However, most type systems operate on
		  high-level languages and calculi, and low-level languages
		  have not received much attention in studies of secure
		  information flow. Therefore, we introduce an information
		  flow type system for a low-level language featuring jumps
		  and calls, and show that the type system enforces
		  termination-insensitive non-interference.

		  Furthermore, information flow type systems for low-level
		  languages should appropriately relate to their counterparts
		  for high-level languages. Therefore, we introduce a
		  compiler from a high-level imperative programming language
		  to our low-level language, and show that the compiler
		  preserves information flow types.}
}

@InProceedings{	  barthe.g.dargenio.p.ea:secure-information-flow-by-self-composition,
  author	= {G. Barthe and P. D'Argenio and T. Rezk},
  title		= {{Secure Information Flow by Self-Composition}},
  editor	= {R. Foccardi},
  booktitle	= {Proceedings of CSFW'04},
  pages		= {100-114},
  publisher	= {IEEE Press},
  year		= {2004},
  abstract	= {Non-interference is a high-level security property that
		  guarantees the absence of illicit information leakages
		  through executing programs. More precisely,
		  non-interference for a program assumes a separation between
		  secret inputs and public inputs on the one hand, and secret
		  outputs and public outputs on the other hand, and requires
		  that the value of public outputs does not depend on the
		  value of secret inputs.

		  A common means to enforce non-interference is to use an
		  information flow type system. However, such type systems
		  are inherently imprecise, and reject many secure programs,
		  even for simple programming languages. The purpose of this
		  paper is to investigate logical formulations of
		  non-interference that allow a more precise analysis of
		  programs. It appears that such formulations are often sound
		  and complete, and also amenable to interactive or automated
		  verification techniques, such as theorem-proving or
		  model-checking.

		  We illustrate the applicability of our method in several
		  scenarii, including a simple imperative language, a
		  non-deterministic language, and finally a language with
		  shared mutable data structures.}
}

@InProceedings{	  barthe.g.prensa-nieto.l:formally,
  author	= {G. Barthe and L. Prensa-Nieto},
  title		= {Formally Verifying Information Flow Type Systems for
		  Concurrent and Thread Systems},
  booktitle	= {Proceedings of FMSE'04},
  editor	= {M. Backes and D. Basin and M. Waidner},
  publisher	= {ACM Press},
  year		= {2004},
  pages		= {13-22},
  abstract	= {Information flow type systems provide an elegant means to
		  enforce confidentiality of programs. Using the proof
		  assistant Isabelle/HOL, we have machine-checked a recent
		  work of Boudol and Castellani, which defines an information
		  flow type system for a concurrent language with scheduling,
		  and shows that typable programs are non-interferent. As a
		  benefit of using a proof assistant, we are able to deal
		  with a more general language than the one studied by Boudol
		  and Castellani. The development constitutes to our best
		  knowledge the first machine-checked account of
		  non-interference for a concurrent language.}
}

@InProceedings{	  barthe.g.rezk.t:non-interference,
  author	= {G. Barthe and T. Rezk},
  title		= {Non-interference for a {JVM}-like language},
  year		= {2005},
  booktitle	= {Proceedings of {TLDI}'05},
  editor	= {G. Morrisett and M. F{\"a}hndrich},
  publisher	= {ACM Press},
  abstract	= {We define an information flow type system for a sequential
		  JVM-like language that includes classes, objects, and
		  exceptions. Furthermore, we show that it enforces
		  non-interference. Our work provides, to our best knowledge,
		  the first analysis that has been shown to guarantee
		  non-interference for a realistic assembly language.}
}

@InProceedings{	  bartoletti.m.degano.p.ea:method,
  author	= {Bartoletti, Massimo and Degano, Pierpaolo and Ferrari,
		  Gianluigi},
  title		= {Method Inlining in Presence of Stack Inspection},
  booktitle	= {Workshop on Issues in the Theory of Security (WITS'04)},
  optcrossref	= {},
  optkey	= {},
  optpages	= {},
  year		= {2004}
}

@InProceedings{	  bartoletti.m.degano.p.ea:policy,
  author	= {Bartoletti, Massimo and Degano, Pierpaolo and Ferrari,
		  Gianluigi},
  title		= {Policy Framings for Access Control},
  booktitle	= {Workshop on Issues in the Theory of Security (WITS'05)},
  optcrossref	= {},
  optkey	= {},
  optpages	= {},
  year		= {2005}
}

@InProceedings{	  bartoletti.m.degano.p.ea:program,
  author	= {Bartoletti, Massimo and Degano, Pierpaolo and Ferrari,
		  Gianluigi},
  title		= {Program Transformations under Dynamic Security Policies},
  booktitle	= {MEPHISTO Final Workshop},
  optcrossref	= {},
  optkey	= {},
  optpages	= {},
  year		= {2004},
  series	= {Electronic Notes in Computer Science},
  volume	= {99},
  optnumber	= {},
  publisher	= {Elsevier},
  optannote	= {}
}

@InProceedings{	  bengtsson.j:generic,
  author	= {Jesper Bengtsson},
  title		= {Generic Implementations of Process Calculi in {I}sabelle},
  booktitle	= {Proceedings of the 16th Nordic Workshop on Programming
		  Theory},
  year		= 2004,
  editor	= {Paul Pettersson and Wang Yi},
  number	= {2004-041},
  pages		= {74-78},
  series	= {IT Technical Reports},
  month		= oct,
  organization	= {Department of Information Technology, Uppsala University},
  abstract	= {Many process calculi have aspects in common, such as
		  parallel composition, name passing and notions of
		  bisimilarity. This abstract covers the beginning of an
		  attempt to create a generic library for these calculi in
		  the automatic theorem prover Isabelle. The goal of the
		  project is to make the library powerful enough to verify
		  both extensions of existing calculi as well as completely
		  new ones.},
  url		= {Available from
		  \url{http://www.it.uu.se/research/reports/2004-041}}
}

@Unpublished{	  boreale.m.buscemi.m.ea:general,
  author	= {Michele Boreale and Marzia Buscemi and Ugo Montanari},
  title		= {A general name binding mechanism},
  note		= {Submitted for publication},
  year		= {2005}
}

@Article{	  boreale.m.buscemi.m:framework,
  author	= {Boreale, Michele and Buscemi, Marzia },
  title		= {A Framework for the Analysis of Security Protocols},
  journal	= {Theoretical Computer Science},
  year		= {2005},
  note		= {To appear}
}

@Unpublished{	  buscemi.m.montanari.u:compositional,
  author	= {Marzia Buscemi and Ugo Montanari},
  title		= {A Compositional Coalgebraic Model of Monadic Fusion
		  Calculus},
  note		= {Submitted for publication},
  year		= {2005}
}

@Unpublished{	  buscemi.m.montanari.u:congruence,
  author	= {Marzia Buscemi and Ugo Montanari},
  title		= {A congruence result for process calculi with structural
		  axioms},
  note		= {Submitted for publication},
  year		= {2005}
}

@Unpublished{	  c.p.saraswat.ea:linearity,
  author	= {Palamidessi C. and Saraswat V. and Valencia, F. and
		  Victor, B.},
  title		= {Linearity vs Persistency in the Pi-Calculus},
  note		= {Ongoing Work},
  optkey	= {},
  optmonth	= {},
  optyear	= {},
  optannote	= {}
}

@Article{	  caires.l.cardelli.l:spatial,
  author	= {L. Caires and L. Cardelli},
  title		= {A spatial logic for concurrency--{II}},
  journal	= {Theor.\ Comput.\ Sci.},
  volume	= {322},
  number	= {3},
  year		= {2004},
  issn		= {0304-3975},
  pages		= {517--565},
  doi		= {http://dx.doi.org/10.1016/j.tcs.2003.10.041},
  publisher	= {Elsevier Science Publishers Ltd.}
}

@Article{	  caires.l.lozes.e:elimination,
  author	= "Luis Caires and Etienne Lozes",
  title		= {Elimination of Quantifiers and Undecidability in Spatial
		  Logics for Concurrency},
  journal	= "Theoretical Computer Science",
  note		= {To appear}
}

@InProceedings{	  caires.l.lozes.e:elimination*1,
  author	= {L. Caires and E. Lozes},
  title		= {Elimination of quantifiers and undecidability in spatial
		  logics for concurrency},
  booktitle	= {Proc.\ of CONCUR'04},
  series	= {Lecture Notes in Computer Science},
  number	= {3170},
  pages		= {240--257},
  publisher	= {Springer Verlag},
  year		= 2004
}

@InProceedings{	  caires.l:behavioral,
  author	= {L. Caires},
  title		= {Behavioral and Spatial Properties in a Logic for the
		  Pi-Calculus},
  booktitle	= {Proc.\ of Foundations of Software Science and Computation
		  Structures'2004},
  series	= {Lecture Notes in Computer Science},
  editor	= {Igor Walukiwicz},
  publisher	= {Springer Verlag},
  year		= 2004
}

@InProceedings{	  dantchev.s.valencia.f:on,
  author	= {S. Dantchev and F. Valencia},
  title		= {On Infinite {CSP}'s},
  booktitle	= {In proceedings of the Third International Workshop on
		  Modelling and Reformulating {CSP}s},
  year		= {2004}
}

@InProceedings{	  deng.y.palamidessi.c:axiomatizations,
  author	= {Yuxin Deng and Catuscia Palamidessi},
  title		= {Axiomatizations for probabilistic finite-state behaviors},
  booktitle	= {Proceedings of the 8th International Conference on
		  Foundations of Software Science and Computation
		  Structures},
  publisher	= {Springer},
  series	= {Lecture Notes in Computer Science},
  year		= {2005},
  note		= {To appear}
}

@InProceedings{	  deng.y.palamidessi.c:axiomatizations*1,
  author	= {Yuxin Deng and Catuscia Palamidessi},
  title		= {Axiomatizations for probabilistic finite-state behaviors},
  booktitle	= {Proceedings of the 8th International Conference on
		  Foundations of Software Science and Computation
		  Structures},
  publisher	= {Springer},
  series	= {Lecture Notes in Computer Science},
  year		= {2005},
  note		= {To appear},
  abstract	= {We study a process calculus which combines both
		  nondeterministic and probabilistic behavior in the style of
		  Segala and Lynch's probabilistic automata. We consider
		  various strong and weak behavioral equivalences, and we
		  provide complete axiomatizations for finite-state
		  processes, restricted to guarded definitions in case of the
		  weak equivalences. We conjecture that in the general case
		  of unguarded recursion the ``natural'' weak equivalences
		  are undecidable.

		  This is the first work, to our knowledge, that provides a
		  complete axiomatization for weak equivalences in the
		  presence of recursion and both nondeterministic and
		  probabilistic choice.}
}

@InProceedings{	  deng.y.sangiorgi.d:ensuring,
  author	= {Yuxin Deng and Davide Sangiorgi},
  title		= {Ensuring termination by typability},
  booktitle	= {Proceedings of the 3rd IFIP International Conference on
		  Theoretical Computer Science},
  publisher	= {Kluwer},
  pages		= {619--632},
  year		= {2004},
  abstract	= {A term terminates if all its reduction sequences are of
		  finite length. We show four type systems that ensure
		  termination of well-typed $\pi$-calculus processes. The
		  systems are obtained by successive refinements of the types
		  of the simply typed $\pi$-calculus. For all (but one of)
		  the type systems we also present upper bounds to the number
		  of steps well-typed processes take to terminate. The
		  termination proofs use techniques from term rewriting
		  systems.

		  We show the usefulness of the type systems on some
		  non-trivial examples: the encodings of primitive recursive
		  functions, the protocol for encoding separate choice in
		  terms of parallel composition, a symbol table implemented
		  as a dynamic chain of cells. }
}

@InProceedings{	  deng.y.sangiorgi.d:towards,
  author	= {Yuxin Deng and Davide Sangiorgi},
  title		= {Towards an algebraic theory of typed mobile processes},
  booktitle	= {Proceedings of the 31th International Colloquium on
		  Automata, Languages and Programming},
  publisher	= {Springer},
  series	= {Lecture Notes in Computer Science},
  volume	= {3142},
  pages		= {445--456},
  year		= {2004},
  abstract	= {The impact of types on the algebraic theory of the
		  $\pi$-calculus is studied. The type system has capability
		  types. They allow one to distinguish between the ability to
		  read from a channel, to write to a channel, and both to
		  read and to write. They also give rise to a natural and
		  powerful subtyping relation.

		  Two variants of typed bisimilarity are considered, both in
		  their late and in their early version. For both of them,
		  proof systems that are sound and complete on the closed
		  finite terms are given. For one of the two variants, a
		  complete axiomatisation for the open finite terms is also
		  presented. }
}

@Article{	  deng.y.sangiorgi.d:towards*1,
  author	= {Yuxin Deng and Davide Sangiorgi},
  title		= {Towards an algebraic theory of typed mobile processes},
  journal	= {Theoretical Computer Science},
  year		= {2005},
  note		= {To appear},
  abstract	= {The impact of types on the algebraic theory of the
		  $\pi$-calculus is studied. The type system has capability
		  types. They allow one to distinguish between the ability to
		  read from a channel, to write to a channel, and both to
		  read and to write. They also give rise to a natural and
		  powerful subtyping relation.

		  Two variants of typed bisimilarity are considered, both in
		  their late and in their early version. For both of them,
		  proof systems that are sound and complete on the closed
		  finite terms are given. For one of the two variants, a
		  complete axiomatisation for the open finite terms is also
		  presented. }
}

@InProceedings{	  ferrari.g.lluch-lafuente.a:a-logic-for-graphs-with-qos,
  author	= {Ferrari, Gianluigi and Lluch-Lafuente, Alberto},
  title		= {{A Logic for Graphs with QoS}},
  booktitle	= {First International Workshop on Views On Designing Complex
		  Architectures},
  optcrossref	= {},
  optkey	= {},
  optpages	= {},
  year		= {2004},
  series	= {Electronic Notes in Computer Science},
  optvolume	= {},
  optnumber	= {},
  address	= {Bertinoro, Italy},
  month		= sep,
  optorganization={},
  publisher	= {Elsevier},
  note		= {To appear},
  optannote	= {}
}

@InProceedings{	  ferrari.g.montanari.u.ea:model-checking-for-nominal-calculi,
  author	= {Ferrari, Gianluigi and Montanari, Ugo and Tuosto, Emilio},
  title		= {{Model Checking for Nominal Calculi}},
  booktitle	= {FOSSACS},
  year		= {2005},
  series	= {LNCS},
  address	= {Edinburgh, UK},
  publisher	= {Springer},
  note		= {To appear}
}

@InProceedings{	  ferrari.g.montanari.u.ea:verification,
  author	= {Ferrari, Gianluigi and Montanari, Ugo and Tuosto, Emilio},
  title		= {Verification on the WEB of Name-Passing Process Calculi},
  booktitle	= {Workshop on Software Engineering Tools: Compatibility and
		  Integration, Monterey Workshop Series},
  year		= {2004},
  series	= {LNCS},
  note		= {To appear}
}

@Unpublished{	  gadducci.f.miculan.m.ea:about,
  author	= {Gadducci, Fabio and Miculan, Marino and Montari, Ugo},
  title		= {About permutation algebras, (pre)sheaves and named sets},
  note		= {Submitted for publication, International Journal on
		  Higher-Order and Symbolic Computation},
  optkey	= {},
  optmonth	= {},
  year		= {2004},
  optannote	= {}
}

@InProceedings{	  ghani.n.yemane.k.ea:relationally,
  author	= {Neil Ghani and Kidane Yemane and Bj{\"o}rn Victor},
  title		= {Relationally Staged Computations in Calculi of Mobile
		  Processes},
  booktitle	= {Proceedings of CMCS 2004 (7th International Workshop on
		  Coalgebraic Methods in Computer Science)},
  series	= {ENTCS},
  volume	= {106},
  publisher	= {Elsevier},
  pages		= {105-120},
  year		= {2004},
  address	= {Barcelona, Spain}
}

@InProceedings{	  hirschkoff.d.pous.d.ea:efficient,
  author	= {D. Hirschkoff and D. Pous and D. Sangiorgi},
  title		= {An {E}fficient {A}bstract {M}achine for {S}afe
		  {A}mbients},
  number	= {2004--63},
  booktitle	= {Proc. of {COORDINATION}~'05},
  year		= {2005},
  note		= {To appear}
}

@InProceedings{	  hirschkoff.d:extensional,
  title		= {An Extensional Spatial Logic for Mobile Processes},
  author	= {D. Hirschkoff},
  booktitle	= {Proc. of CONCUR'04},
  year		= 2004,
  pages		= {325--339},
  volume	= 3170,
  publisher	= {Springer Verlag}
}

@PhDThesis{	  lozes.e:expressivite,
  author	= {E. Lozes},
  title		= {Expressivit{\'e} des logiques d'espaces},
  school	= {{\'E}cole Doctorale MathInf, ENS Lyon},
  year		= 2004
}

@InProceedings{	  lozes.e:separation,
  author	= {E. Lozes},
  title		= {Separation logic preserves the expressive power of
		  classical logic},
  booktitle	= {Proc.\ Workshop Space'04},
  note		= {Electronic publication},
  year		= 2004
}

@InProceedings{	  martins.f.ravara.a:typing,
  author	= {F. Martins and A. Ravara},
  title		= {Typing Migration Control in Lsdpi},
  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{	  miculan.m.yemane.k:unifying,
  author	= {Marino Miculan and Kidane Yemane},
  title		= {A Unifying Model of Variables and Names},
  booktitle	= {Proceedings of FOSSACS'05},
  year		= {2005},
  series	= {LNCS},
  publisher	= {Springer},
  note		= {To appear}
}

@InProceedings{	  montanari.u:web,
  author	= {Montanari, Ugo},
  title		= {Web Services and Models of Computation},
  booktitle	= {First International Workshop on Web Services and Formal
		  Methods},
  optcrossref	= {},
  optkey	= {},
  optpages	= {},
  year		= {2004},
  series	= {Electronic Notes in Computer Science},
  volume	= {105},
  optnumber	= {},
  publisher	= {Elsevier},
  optannote	= {}
}

@Unpublished{	  pous.d:gcpan,
  author	= {D. Pous},
  title		= {{GCPAN} Implementation},
  note		= {\url{http://perso.ens-lyon.fr/damien.pous/gcpan}},
  year		= {2004}
}

@TechReport{	  ribeiro.a.caires.l.ea:verifying-the-arrow-protocol-in-a-spatial-logic,
  author	= "A. Ribeiro and L. Caires and L. Monteiro",
  title		= "{Verifying the Arrow Protocol in a Spatial Logic}",
  institution	= {Departamento de Informatica, FCT/UNL},
  number	= {TR-DI/FCT/UNL-04/2004},
  year		= 2004
}

@InProceedings{	  teller.d:recovering,
  author	= {D. Teller},
  title		= {Recovering resources in the pi-calculus},
  year		= 2004,
  booktitle	= {Proceedings of IFIP TCS 2004},
  publisher	= {Kluwer},
  abstract	= {Although limits of resources such as memory or disk usage
		  are one of the key problems of many communicating
		  applications, most process algebras fail to take this
		  aspect of mobile and concurrent systems into account. In
		  order to study this problem, we introduce the Controlled
		  pi-calculus, an extension of the pi-calculus with a notion
		  of recovery of unused resources with an explicit
		  (parametrized) garbage-collection and dead-process
		  elimination. We discuss the definition of
		  garbage-collection and dead-process elimination for
		  concurrent, communicating applications, and provide a
		  type-based technique for statically proving resource
		  bounds. Selected examples are presented and show the
		  potential of the Controlled pi-calculus.},
  url		= {http://perso.ens-lyon.fr/david.teller/recherche/Publications/cpil.pdf}

}

@PhDThesis{	  teller.d:ressources,
  author	= {Teller, D.},
  title		= {Ressources limit{\'e}es pour la mobilit{\'e}: utilisation,
		  r{\'e}utilisation, garanties},
  school	= {{\'E}cole doctorale MathIF, ENS Lyon},
  year		= {2004},
  type		= {{PhD} thesis}
}

@InProceedings{	  tuosto.e.vieira.h:an-observational-model-for-spatial-logics,
  author	= {Tuosto, Emilio and Vieira, {Hugo T.}},
  title		= {{An Observational Model for Spatial Logics}},
  booktitle	= {First International Workshop on Views On Designing Complex
		  Architectures},
  year		= {2004},
  series	= {ENTCS},
  address	= {Bertinoro, Italy},
  month		= sep,
  publisher	= {Elsevier},
  note		= {To appear}
}

@InProceedings{	  tuosto.e:tarzan--communicating-and-moving-in-wireless-jungles,
  author	= {Tuosto, Emilio},
  title		= {{Tarzan: Communicating and Moving in Wireless Jungles}},
  booktitle	= {2nd Workshop on Quantitative Aspects of Programming
		  Languages},
  pages		= {77--94},
  year		= {2004},
  editor	= {Cerone, A. and {Di Pierro}, Alessandra},
  volume	= {112},
  series	= {Electronic Notes in Computer Science},
  publisher	= {Elsevier}
}

@TechReport{	  vallecillo.a.vasconcelos.vt.ea:typing,
  author	= {Antonio Vallecillo and Vasco T. Vasconcelos and Ant\'onio
		  Ravara},
  title		= {Typing the Behavior of Software Components using Session
		  Types},
  year		= 2004,
  month		= dec,
  url		= {http://www.di.fc.ul.pt/~vv/papers/newsessiontypes.pdf},
  note		= {Revised and extended version of Typing the Behavior of
		  Objects and Components using Session Types. In Foclasa
		  2002, 1st International Workshop on Foundations of
		  Coordination Languages and Software Architectures.
		  Electronic Notes in Theoretical Computer Science, 68(3),
		  2002.}
}

@PhDThesis{	  vanackere.v:trust--un-systeme-de-verification-automatique-de-protocole-cryptographique,
  author	= {Vanackere, Vincent},
  title		= {{TRUST: un systeme de verification automatique de
		  protocole cryptographique}},
  school	= {Universit{\'e} de Provence},
  year		= 2005
}

@InProceedings{	  vasconcelos.vt.ravara.a.ea:session,
  author	= {Vasco T. Vasconcelos and Ant\'onio Ravara and Simon Gay},
  title		= {Session types for functional multithreading},
  booktitle	= {CONCUR'04},
  pages		= {497--511},
  year		= 2004,
  volume	= 3170,
  series	= lncs,
  publisher	= springer,
  url		= {http://www.di.fc.ul.pt/~vv/papers/stfm.pdf}
}

@InProceedings{	  zilio.sd.lugiez.d.ea:logic,
  author	= {S. Dal Zilio and D. Lugiez and C. Meyssonnier},
  title		= {A Logic you Can Count On},
  booktitle	= {{POPL}~2004 -- 31st Annual ACM SIGPLAN-SIGACT Symposium on
		  Principles of Programming Languages},
  publisher	= {ACM Press},
  year		= 2004
}