Subtyping and typing algorithms for mobile ambients

The ambient calculus was designed to model mobile processes and study their properties. A first type system was proposed by Cardelli-Gordon-Ghelli to prevent run-time faults. We extend it by introducing subtyping and present a type-checking algorithm which returns a minimal type relatively to this system. By the way, we also add two new constructs to the language. Finally, we remove the type annotations from the syntax and give a type-inference algorithm for the original type system.