Ce livre introduit les semantiques formelles et detaille des exemples d'utilisation pour definir des langages de programmation realistes et verifier des proprietes semantiques de ces langages. Il presente plusieurs styles et plusieurs definitions de semantiques formelles, puis introduit differentes transformations de programmes, et expose les choix de conception associes. En particulier, ce livre decrit une transformation de programmes inspiree de l'evaluation partielle et dediee a la comprehension de programmes scientifiques. Il detaille egalement le front-end d'un compilateur moderement optimisant du langage C dedie au logiciel embarque critique, ayant ete formellement verifie avec l'assistant a la preuve Coq et developpe dans le cadre du projet CompCert."