SafeDpi est un langage d'ordre supérieure, basé sur le π-calcul, qui permet d'exprimer le comportement des agents mobiles qui se déplacent entre les sites d'un réseau réparti.
Dans cet exposé nous présentons un système de types sophistiqué qui permet de contrôler l'accès de ces agents mobiles à des ressources locales, et plus généralement de contrôler leur comportement quand ils visitent un site. À travers des types dépendants et existentiels les sites hôtes peuvent se protéger contre des agents douteux. En contre partie les agents migrants ont le contrôle de la visibilité de leur état interne.
Si nous en avons le temps, nous présenterons également une notion de bisimulation pour le langage SafeDpi qui caractérise l'équivalence comportementale naturelle, basée sur des contextes. Ces bisimulations utilisent des actions typées qui formalisent l'idée d'un environnement expérimentale qui accumule des connaissances sur le comportement des systèmes.