CTL
14 mai 2009 - 14h00
ASPfun: un calcul pour des objets distribués
par Florian Kammueller de Technische Universitat Berlin
Résumé : La programmation d'un grand réseau d' ordinateurs distribués,
tel que l'Internet, pose de nouveaux problèmes de sécurité.
Je présente dans cet exposé le langage formel ASPfun pour les
objets distribués asynchrones.
ASPfun élargit la théorie des objets par une communication requêtes-réponse basée sur des futurs. Un futur représente le
résultat encore attendu d'une requête donnée; la réponse exprime
le résultat d'une requête à l'objet qui contient le futur.
Ma présentation introduit le calcul ASPfun et sa sémantique.
Je résume nos résultats sur les systèmes de typage et la
sûreté des types d'ASPfun. ASPfun et toutes ses propriétés sont entiérement formalisées et demontrées avec l'assistant de preuve Isabelle/HOL.
candidat sur le poste INPG
