Résumé
Le quatrième séminaire a approfondi la mécanisation d’une logique de séparation, sujet que le quatrième cours avait juste effleuré. Le conférencier a montré comment construire une telle logique en Coq à partir d’une sémantique naturelle pour un petit langage de type « mini-ML », c’est-à-dire un langage fonctionnel étendu avec des références mutables. Il a ensuite décrit plusieurs outils, toujours intégrés dans Coq, qui facilitent les vérifications de programmes : un calcul de plus faible précondition, des prédicats d’encodage de structures de données, et des tactiques Coq. Tous ces éléments se retrouvent dans son outil CFML de vérification de programmes impératifs.
