Précédent : Normalisation forte Remonter : Résultats nouveaux Suivant : Micro-paiements en commerce éléctronique
Précédent : Normalisation forte
Remonter : Résultats nouveaux
Suivant : Micro-paiements en commerce éléctronique
Mots clés : Ramasse-miettes, algorithmique distribuée, analyse statique, non-interférence, systèmes de types purs .
La formalisation en Coq de la preuve de correction et de vivacité de l'algorithme de comptage de références distribué dû à L. Moreau a été achevée. Ce travail est exposé dans un papier soumis a Acta Informaticae, et enregistré comme rapport de recherche du laboratoire Lip []. Par ailleurs, le code de la preuve fait partie de la distribution du système Coq, au titre de contribution. En utilisant des abstractions sur les sortes, F. Prost est arrivé à formaliser la notion de non-interférence, qui est une notion centrale en analyse, pour des langages d'ordres supérieurs. Il a présenté ces résultats à la conférence internationale CADE [] dont une pré-version a été réalisée sous la forme d'un rapport de recherche : []. D'autre part, il a soutenu sa thèse «Interprétation de l'analyse statique en théorie des types» sur ce sujet.