Le plan du cours change d'année en année. Vous pouvez accéder au cours tel que je l'avais fait (ou avais prévu de le faire) en 2000-2001, 2001-2002, 2002-2003, 2003-2004, 2004-2005, 2005-2006, 2006-2007, 2007-2008, 2008-2009.

Cours de sémantique (année 2009-2010)

Dans ce cours nous voulons que les étudiants apprennent à réfléchir sur le sens des programmes et le pouvoir expressif des langages de programmation. Ce cours repose sur une fondation théorique importante: vous devrez maîtriser des notions de logique et de calculabilité. Mais les applications pratiques de ce cours sont spectaculaires: c'est grâce aux concepts abordés dans ce cours que l'on est capable de mettre au point du logiciel critique, utilisable en avionique, en commerce électronique, ou en transport ferroviaire. Une bonne maîtrise de la sémantique des langages de programmation permet en effet de développer des compilateurs auxquels on peut faire confiance, des outils de vérification automatique pour éviter les erreurs de débordement, les trous de sécurité, etc, et des outils pour spécifier le comportement attendu du logiciel et vérifier que les programmes respectent leurs spécifications.

1. apprentissage du système Coq (trois séances)

Dans la première partie du cours, nous apprendrons à nous servir d'un système de démonstration sur ordinateur. Nous utiliserons ensuite ce système de démonstration sur ordinateur pour décrire précisément un petit langage de programmation, pour développer des outils manipulant des programmes de ce langage de programmation, et pour montrer que ces outils sont corrects, au sens où il permettent d'éviter l'introduction d'erreurs de programmation ou de détecter certaines classes d'erreurs.

Les notes pour le premier cours sont disponibles ici .

Pas de TD la première semaine

TD pour la deuxième semaine

Tout est dans le fichier suivant: sem2010td1.v

Voici la solution : sem2010td1sol.v

Devoir à la maison pour la première semaine

écrivez la fonction sop5 qui additionne les premieres puissances cinquièmes:

 1 + 32 + 243 + ... +n^5

Trouvez une formule de la forme : forall x, k*sop5 x = l*x^6 + .... puis démontrez que cette formule est correcte. Tout doit être fait dans Coq. (inspirez-vous de l'exemple sos).

Quelques liens utiles:

TD pour la troisième semaine

Tout est dans le fichier suivant: sem2010td2.v

Voici la solution.

2. Syntaxe et sémantique naturelle

Dans cette partie du cours nous montrons comment décrire les structures syntaxiques d'un petit langage de programmation. Ensuite nous montrons comment décrire le comportement des instructions de ce langage. Nous concluons en montrant comment tout ce travail peut être implémenté dans Coq. Le cours est principalement basé sur ces notes de cours.

TD pour la quatrième semaine

C'est dans ce fichier.

Correction du TD de la quatrième semaine

C'est dans ce fichier.

Voici la solution.

Cinquième semaine

Cette semaine nous nous concentrerons sur les preuves par récurrence sur les dérivations et les étapes de preuve par inversion.

TD pour la cinquième semaine

La propriété à laquelle nous nous intéressons est l'inverse de la propriété que nous avons vue au td de la quatrième semaine. C'est dans sem2010td5.v.

Voici la solution.

Devoir à la maison pour la cinquième semaine

C'est dans sem2010dm5.v. C'est un devoir qui fait appel au preuves par récurrences sur les dérivations (en Coq, preuves par récurrence sur les propriétés inductives).

Sixième semaine

Cette semaine, nous étudierons les fonctions qui permettent de simuler l'exécution d'un programme

TD pour la sixième semaine

Ce TD est une implémentation directe du cours, il s'agit de montrer que la fonction définie en cours est correcte. Voici le fichier

Voici la solution.