Nous encodons dans Coq un modèle dénotationnel du langage d’entrée de Vélus, compilateur synchrone vérifié. Nous spécifions formellement les conditions de son équivalence avec le modèle relationnel existant, et nous explorons la possibilité d’un raisonnement interactif sur les programmes, à l’aide notamment d’un plongement du nouveau modèle dans celui des réseaux de Kahn.
