In this report we show how we proved correctness of the translation from a small applicative language with recursive definitions (Mini-ML) to the Categorical abstract machine (CAM) using the Coq system. Our aim was to mechanize the proof of J. Despeyroux \cite{Des}. Like her, we use natural semantics to axiomatise the semantics of our languages. We have only partially mecanised the proof. The semantics of the source and target languages use rational trees in their definition and at this stage the Coq system is inefficient in axiomatising such structures. We propose a presentation of the correctness proof to isolate this difficulty.