Ce livre introduit les s mantiques formelles et d taille des exemples d'utilisation pour d finir des langages de programmation r alistes et v rifier des propri t s s mantiques de ces langages. Il pr sente plusieurs styles et plusieurs d finitions de s mantiques formelles, puis introduit diff rentes transformations de programmes, et expose les choix de conception associ s. En particulier, ce livre d crit une transformation de programmes inspir e de l' valuation partielle et d di e la compr hension de programmes scientifiques. Il d taille galement le front-end d'un compilateur mod r ment optimisant du langage C d di au logiciel embarqu critique, ayant t formellement v rifi avec l'assistant la preuve Coq et d velopp dans le cadre du projet CompCert.