08/03/2001: Luca Cardelli (Microsoft Research)
Logical Properties of Name Restriction

Résumé
The ambient calculus is a process calculus based on mobility, where processes reside at the nodes of a dynamic hierarchy of locations. It becomes natural to discuss properties that hold at particular locations, and to discuss the dynamic evolution of the hierarchy of locations. We use a logic as a way of formalizing such descriptions.

We describe a modal logic for the ambient calculus, whose main novelty is the introduction of spatial connectives (in addition to standard and temporal connectives). Our logic can be used for specifying mobility protocols, for expressing mobility policies, and as a playground for model checking of mobile computation, with potential applications to bytecode verification of mobile code.

In our latest development, we have extended our logic to describe systems with hidden/secret locations. To this end, we combine a Gabbay-Pitts fresh-name quantifier with a novel "revelation" operator that can talk about restricted names. The talk will focus on these recent topics.