L'objet de la sémantique est fondamentalement d'associer du sens à des composants d'un langage. Pour nous ce seront les différents éléments d'un programme.
Le sens est un objet mathématique à définir, sur lequel on peut faire des manipulations formelles et des preuves.
Dans la première partie de ce cours, on présentera les deux premières approches classiques d'abord sur le lambda-calcul, parce que c'est plus simple et parce que c'est l'archétype des langages de programmation, puis nous étudierons ces mêmes concepts sur un langage impératif de type Pascal. Enfin nous étudierons la sémantique axiomatique de ce langage.
Pour les travaux dirigés, je vous invite à aller consulter la page d'Étienne Lozes.
Voici l'article de Carl Gunter sur les progammes micro-mobiles dont j'ai parlé. Pour trouver l'article de John Reynolds sur la preuve de programmes avec des références visitez Separation Logic: A Logic for Shared Mutable Data Structures sur sa page
Le formulaire d'évaluation est là.