Cours : Daniel Hirschkoff

TD : Adrien Durier & Alexis Ghyselen & Julien Braine

Il existe de nombreux langages de programmation, et ce foisonnement est sans cesse alimenté par l’apparition de nouveaux langages. Ce cours propose une introduction à un certain nombre de méthodes ouvrant la voie à l’analyse rigoureuse des langages de programmation et des programmes. Ces méthodes fournissent un cadre dans lequel représenter les programmes, et prouver des propriétés sur leur comportement à l’exécution. Ce faisant, il est possible d’analyser des transformations de programmes, d’établir des comparaisons entre langages de programmation, et, plus généralement, de prendre du recul par rapport à la richesse du paysage des langages de programmation.

Les sujets suivants sont traités dans le cours:

  • définitions inductives, sémantique opérationnelle des programmes (pour un mini-langage impératif et un mini-langage fonctionnel)
  • garanties sur l’exécution des programmes: sémantique axiomatique (logique de Floyd-Hoare), typage
  • propriétés abstraites sur l’exécution des programmes, notions de réécriture: terminaison, confluence, unification

Bibliographie

  • G. Winskel, The semantics of programming languages, MIT Press.
  • J. Reynolds, Theories of Programming Languages, CUP.
  • F. Baader et T. Nipkow, Term Rewriting and All That, Cambridge University Press
  • une page web liée au cours sera disponible à partir de la page http://perso.ens-lyon.fr/daniel.hirschkoff

Le cours est organisé selon le schéma hebdomadaire suivant: 2h de cours; 2h de travaux pratiques sur machine ou de travaux dirigés. En travaux pratique, une initiation à l’assistant de preuves Coq sera
proposée.

Prérequis: une expérience de la programmation, quel que soit le langage, est souhaitée.