INF 565 : Systèmes de Preuves

2011

Benjamin Werner

Cyril Cohen

Horaires: Vendredi, PC 41: 13h30-15h, TD salle info 35, 15h15-17h15.

Documentation

Un guide de survie pour les tactiques ssr de Coq.

Tactique pratique

La tactique  myo est definie dans les fichier:  /users/profs/info/werner/COQ Elle permet de resoudre certains buts comportant des egalites et inegalites entre entiers naturels et relatifs.

Cours

Les solutions données ne sont qu'une possibilité parmi d'autres. Elles sont souvent formulées de manière à illustrer certaines possibilités du langage de preuve. 

PC1 (2010)    TD1 Solution

TD2 (Le Damier de Cachan)

TD3, le tri: exercice et solution.

Formalisation de PCF; squelette et une solution

exo reflection puis types dans PCF. Une solution.

Compilation: Le rapport de recherche de X. Leroy; le chapitre 3 est une bonne présentation de la machine abstraite KAM et de sa preuve de correction. Une version de départ possible pour la preuve de correction.

Projets

Pour le projet, deux propositions:

1) Partir du corrigé, de la correction de la KAM vis-à-vis de la sémantique à petits pas, et étendre la machine:

* Transformer la machine en appel par valeurs. Pour cela, ajouter l'instruction reduce, telle que décrite à la page 27 du rapport ZINC.

Etendre la machine se fait simplement en suivant le texte du rapport. Il faut réfléchir un peu pour définir la décompilation des piles.

On peut ensuite reprendre les preuves en ajoutant les nouveaux cas. Il n'y a pas trop de pièges.

* On peut ensuite ajouter les entiers primitifs et les opérateurs. Cela demande de réfléchir ou chercher un peu pour trouver une machine qui traite les entiers.

Attention, il vaut mieux réflechir d'abord à la machine, puis proposer une extension du langage source qui permette de bien définir la décompilation. Ensuite faire les preuves.

* Enfin on peut ajouter ensuite le test à zéro.

2) Définir une sémantique à grands pas en suivant le chapitre 3 du cours de G. Dowek. On le faire soit pour le langage riche (des premiers TDs), soit le langage réduit (que l'on a compilé).

Il est sans doute plus facile de le faire pour le langage réduit. Dans ce cas, on peut continuer en prouvant la correction de la KAM par rapport à cette sémantique.


28-01-2010