Reproduction de : Thèse de doctorat : Physique (option optoélectronique) : Metz : 2002. / Titre provenant de l'écran-titre. Notes bibliographiques.

Thèse (Ph.D.)--Université Laval, 2008. / Bibliogr.: [241]-263. Publié aussi en version électronique dans la Collection Mémoires et thèses électroniques.

Thèse doctorat : Physique : Strasbourg 1 : 2006. / Titre provenant de l'écran-titre. Bibliogr. 9 p.

Thèses (M.Sc.)--Université de Sherbrooke (Canada), 2000. / Titre de l'écran-titre (visionné le 20 juin 2006). Publié aussi en version papier.

Th. 3e cycle--Inform.--Rennes 1, 1979. N°: 585.

Reproduction de : Thèse de doctorat : Lasers, Molécules et Rayonnement atmosphérique : Lille 1 : 2005. / N° d'ordre (Lille 1) : 3662. Résumé en français et en anglais. Titre provenant de la page de titre du document numérisé. Bibliogr. p. 219-229. Liste des publications.

Thèse de doctorat : Ingénierie Cellulaire et Tissulaire : Nancy 1 : 2008. / Titre provenant de l'écran-titre.

Reproduction de : Thèse de doctorat : Physique : Lyon 1 : 2007. / Titre provenant de l'écran titre. 210 réf. bibliogr.

Thèse (M.Th.) -- Université du Québec à Chicoutimi, programme extensionné de l'Université de Montréal, 2005. / Bibliogr.: f. [173-177].

Les outils d'aide à la preuve basés sur la théorie des types permettent à l'utilisateur d'adopter soit un style fonctionnel, soit un style relationnel (c'est-à-dire en utilisant des types inductifs). Chacun des deux styles a des avantages et des inconvénients. Le style relationnel peut être préféré parce qu'il permet à l'utilisateur de décrire seulement ce qui est vrai, de s'abstraire temporairement de la question de la terminaison, et de s'en tenir à une description utilisant des règles. Cependant, une spécification relationnelle n'est pas exécutable.Nous proposons un cadre général pour transformer une spécification inductive en une spécification fonctionnelle, en extrayant à partir de la première une fonction et en produisant éventuellement la preuve de correction de la fonction extraite par rapport à sa spécification inductive. De plus, à partir de modes définis par l'utilisateur, qui permettent de considérer les arguments de la relation comme des entrées ou des sorties (de fonction), nous pouvons extraire plusieurs comportements calculatoires à partir d'un seul type inductif.Nous fournissons également deux implantations de notre approche, l'une dans l'outil d'aide à la preuve Coq et l'autre dans l'environnement Focalize. Les deux sont actuellement distribuées avec leurs outils respectifs.