The need for formal methods for certifying the good behaviour of computer software is dramatically increasing with the growing complexity of the latter. Moreover, in the global computing framework one must face the additional issues of concurrency and mobility. In the recent years many new process algebras have been introduced in order to reason formally about these problems; the common pattern is to specify a type system which allows one to discriminate between *good" and "bad" processes. In this paper we focus on an incremental type system for a variation of the Ambient Calculus called M 3, i.e., Mobility types for Mobile processes in Mobile ambients and we formally prove its soundness in the proof assistant Coq.
