PROG – Théorie de la Programmation (1er semestre, 6 ECTS)

Cours : Philippe Audebaud

TD :  Anupam Das & Fabrice Mouhartem & Antoine Plet

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/philippe.audebaud/

Le cours est organisé selon le schéma hebdomadaire suivant: 2h de cours; 2h de travaux pratiques sur machine ou de travaux dirigés; un partiel, un examen, des devoirs à la maison. Une partie des TPs sur machine s’appuie sur le système d’aide à la preuve Abella (une initiation à Abella sera proposée).

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

Leave a Reply

You can use these HTML tags

<a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>