Abstract FR:

Dans le cadre de la generation de compilateurs dirigee par la semantique, se pose le probleme de transformer une semantique source d'un langage de programmation en une semantique objet equivalente, plus proche d'une implementation. La plupart des travaux dans ce domaine resolvent ce probleme de facon non constructive: une semantique objet est d'abord exhibee, ensuite prouvee correcte vis-a-vis de la semantique source. Le but de cette these est de montrer qu'on peut deriver une semantique objet a partir d'une semantique source d'un langage, de maniere constructive, tout en preservant certains criteres de correction fixes au depart