Global ETD Search

1	Extraction de programmes dans le Calcul des Constructions Paulin-Mohring, Christine 27 January 1989 (has links) (PDF) Cette thèse propose une extension du Calcul des Constructions de Coquand et Huet qui permet l'extraction de programmes certifiés à partir de preuve constructive. Une notion de réalisabilité modifiée est introduite et étudiée. Un codage imprédicatif d'une large classe de définitions inductives est proposé. Théorie des Types Realisabilité Extraction de programmes Preuves constructives Définitions inductives
2	Logique du temps arborescent pour la spécification et la preuve de programmes Graf, Susanne 29 February 1984 (has links) (PDF) Nous étudions les logiques du temps arborescent en tant qu'outils de spécification et de preuve des programmes. Les différentes logiques modales et temporelles sont comparées par rapport aux deux critères suivantes: puissance d'expression et décidabilité. Cette étude porte essentiellement sur fa comparaison des logiques du temps arborescent et des logiques du temps linéaire. Ensuite, le problème de l'utilisation des logiques du temps arborescent en tant qu'outils de preuves des programmes est étudié. Nous proposons une logique pour la preuve constructive des propriétés des processus contrôlables de CCS. Cette logique est telle, que la relation de congruence induite est la congruence observationnelle de CCS Spécification de programmes preuve de programmes logique temporelle temps linéaire temps arborescente puissance d'expression axiomatisation procédure de décision CCS preuves constructives

Search results

Extraction de programmes dans le Calcul des Constructions

Logique du temps arborescent pour la spécification et la preuve de programmes