Le système Centaur permet la description d'un langage de programmation en Sémantique Naturelle. Cette description peut être exécutée (en Prolog) et testée puis traduite en données pour le système Coq pour permettre la réalisationde preuves de propriétés de cette sémantique. Nous présentons ici les premiers pas dans l'application de cette approche aux langages à objets en s'appuyant sur le sigma-calcul défini par M.~Abadi et L.~Cardelli dans leur livre A Theory of Objects. La réalisation en Coq de la preuve de conservation des types (SRT) pour le sigma-calcul avec récursion et sous-typage (Ob1