Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Programmer de manière sûre avec des types dépendants dans Coq
Programmer de manière sûre avec des types dépendants dans Coq
1 Contexte
Le Calcul des Constructions Inductives qui sert de base à l'assistant
de preuve Coq fournit un langage de description de programmes et de
preuves puissant. Des programmes fonctionnels peuvent être vus comme
des descriptions partielles de preuves de propriétés.
Par exemple un programme de division euclidienne peut se voir comme une
preuve de la propriété :
" a,b. b ³ 0 Þ $ q,r. a=bq+r Ù r<b
Reposant sur cette idée, une tactique Program avait été réalisée par
C. Parent. Cette tactique repose essentiellement sur une inversion de
la procédure d'extraction de programmes à partir de preuves et n'est
actuellement plus supportée par les nouvelles versions de Coq. Le
système PVS propose une méthode alternative : la génération de
Type Checking Conditions (TCC). Cette notion repose sur la
présence dans la théorie d'un type sous-ensemble {x:t
| P(x)}. Un élement a aura pour type {x:t
| P(x)} si une preuve de P(a) peut être dérivée.
2 Objet du stage
Le but du stage est de mettre en place un langage de programmation
sûre avec des types dépendants dans Coq. L'utilisateur doit pouvoir
enrichir ses types de données à l'aide d'assertions logiques, puis
construire des termes dans ces types dépendants, dans un langage
proche des langages de programmation. L'écriture d'un programme peut
engendrer des obligations de preuves à résoudre.
En partant de l'expérience de la tactique Program et des
TCC de PVS, l'étudiant formalisera une interprétation des
programmes permettant d'engendrer des obligations de preuves.
Contrairement à Program cette interprétation ne devrait pas
être directement liée à l'extraction de programme mais être vue comme
un enrichissement du langage de description de CCI.
Contrairement aux TCC de PVS, ce langage devra prendre en
compte la richesse du langage de types dépendants de CCI et pas
uniquement les types sous-ensembles.
3 Prérequis
Connaissance de la théorie des types et plus particulièrement du
Calcul des Constructions Inductives.
4 Contact
Christine Paulin-Mohring LRI-Bat 490 Université Paris Sud 91405 Orsay cedex tel 01 69 15 66 35 Christine.Paulin@lri.fr
S. Owre, N. Shankar, J. M. Rushby, and D. W. J.Stringer-Calvert.
PVS Language Reference.
Computer Science Laboratory, SRI International, Menlo Park, CA,
September 1999.
C. Parent.
Developing certified programs in the system Coq- The Program
tactic.
volume 806 of Lecture Notes in Computer Science, Nijmegen,
1994. Springer-Verlag.