Abstract FR:

Les systemes communicants mettent en jeu des objets potentiellement infinis (boucles d'interaction, listes de donnees infinies, espaces d'etats infinis, etc. ). L'etude de tels systemes informatiques semble necessiter un cadre logique ou on soit capable de decrire et de raisonner sur ces objets. Dans cette these, nous developpons une extension du calcul des constructions avec des types qui contiennent des objets infinis (dits types co-inductifs). Notre calcul se base sur les schemas de definitions recursives gardees developpes par thierry coquand dans le cadre de la theorie des types de martin-lof. A la difference de celle proposee par t. Coquand, notre extension est compatible avec la quantification impredicative presente dans le calcul des constructions, et preserve la propriete de normalisation forte, indispensable pour son implantation. Nous illustrons ses potentialites comme cadre logique pour la verification de systemes reactifs par l'etude d'un protocole de communication de donnees. Nous avons certifie ce protocole en utilisant l'editeur de preuves coq, dans lequel nous avons implante notre extension