Résumé
Le premier cours a débuté par un bref historique des sémantiques formelles pour les langages de programmation. Les premiers langages de programmation de haut niveau font apparaître des points délicats de sémantique : le passage d’arguments aux fonctions en Algol 60, « par nom » ou bien « par valeur », et la liaison des variables en Lisp, avec sa sémantique de liaison dynamique qui sera remplacée plus tard par la liaison statique.
En partie pour éclaircir ces points délicats, en partie pour faciliter le raisonnement sur les programmes, les premières sémantiques formelles apparaissent dès le milieu des années 1960, suivant trois styles différents qui sont toujours bien vivants aujourd’hui : les sémantiques opérationnelles, avec les travaux précurseurs de Landin en 1964 et beaucoup d’utilisations depuis 1990 ; les sémantiques axiomatiques, introduites par Floyd en 1967, et développées par Hoare, Dijkstra et coauteurs pendant les années 1970 ; les sémantiques dénotationnelles, introduites sous une forme simplifiée par Strachey vers 1965 puis mathématiquement fondées sur la théorie des domaines par Scott et coauteurs entre 1970 et 1990.
Ensuite, le cours a introduit le petit langage de programmation IMP qui a servi d’objet d’étude dans la plupart des cours de cette année. C’est un langage impératif, structuré en expressions arithmétiques, expressions booléennes, et commandes qui modifient des variables de type entier. Les expressions se prêtent merveilleusement à une sémantique dénotationnelle « naïve » à la manière de Strachey. Les commandes pouvant ne pas terminer, leur sémantique dénotationnelle est plus délicate ; c’est pourquoi nous avons adopté des sémantiques opérationnelles, à réductions comme dans le λ-calcul, ou bien naturelles, ou encore par interpréteur de référence.
Enfin, le cours a motivé le besoin de mécaniser les sémantiques de langages réalistes, c’est-à-dire de s’aider de la puissance de la machine pour écrire ces sémantiques et raisonner à leur propos. Comme exemple de cette démarche, nous avons montré comment mécaniser la syntaxe abstraite et les sémantiques opérationnelles du langage IMP à l’aide de l’assistant à la démonstration Coq. Nous avons finalement démontré des résultats d’équivalence entre la sémantique à réduction, la sémantique naturelle, et l’interpréteur de référence.
