Cminor est un langage de bas niveau proche de C, utilisé comme langage intermédiaire dans un compilateur C certifié en Coq. Cet exposé présente le développement en Coq d'une sémantique axiomatique pour Cminor ainsi que les preuves de correction associées. Cette sémantique constitue un premier lien entre la preuve de programmes et certification de compilateurs. Elle utilise la logique de séparation pour raisonner sur la mémoire et les pointeurs. Elle est définie selon un style à petits pas afin de pouvoir enrichir dans le futur le langage Cminor par des traits concurrents. Cette sémantique est également une sémantique à continuations, ce qui a facilité les preuves de correction.