lieu : ENSTA, amphi Parmantier
La sérialisation (marshaling ou pickling, en Anglais) d'une valeur (résultat d'un calcul) par un programme consiste à la représenter sous la forme d'une suite d'octets de sorte à pouvoir la sauvegarder dans un fichier pour relecture ultérieure ou la communiquer à d'autres programmes via un réseau. Pour sérialiser efficacement, on sauve une représentation linéaire du graphe mémoire de la valeur, en préservant partage et cycles. Manipuler ces valeurs après leur relecture dans un langage typé statiquement impose de leur attribuer un type statique sans risquer de compromettre les propriétés apportées par la discipline de typage du langage. Pour ce faire, on adjoint généralement aux valeurs sérialisées leur type, de sorte à pouvoir vérifier que le type attendu après relecture correspond bien au type effectif de la valeur relue.
Je présenterai dans cet exposé une technique de vérification de typage des valeurs sérialisées qui ne nécessite pas une telle adjonction d'information de type. Je présenterai aussi quelques-uns des éléments de la formalisation qui permet d'en énoncer et en prouver les propriétés.
Il s'agit d'un travail commun avec Grégoire Henry et Emmanuel Chailloux (PPS, Chevaleret, Paris 6).