• Langue : Français
• Discipline : Informatique
• Identifiant : Inconnu
• Type de thèse : Doctorat
• Date de soutenance : 01/01/1990

Résumé en langue originale

Un système de programmation par preuves est présenté. Nous définissons un système formel supposé étendre l'arithmétique de Heyting en tenant compte des types de données interprétés à l'aide d'algèbres de termes. La preuve formelle d'une formule spécifiant un programme permet la construction systématique à partir d'une preuve d'un programme à l'aide de l'interprétation de réalisabilité. Nous raffinons la définition classique d'une telle interprétation par rapport à une propriété syntaxique des formules. Cette nouvelle interprétation permet par rapport à la première l'extraction de programmes relativement efficaces dans la mesure où les réalisants ne retiennent d'une preuve que l'information calculatoire en ignorant l'information qui ne sert qu'à justifier les dérivations. La récurrence dans les preuves cruciales dans la synthèse des programmes récursifs est traitée par une variante effective de la règle de récurrence bien fondée. A un niveau sémantique, une classe de relations bien fondées est définie en tant que domaine effectif dans la théorie des domaines. La description de l'implantation d'un compilateur de preuves est donnée dans la langage CAML de l'INRIA. Des exemples non triviaux illustrent de façon agréable cette approche à la programmation correcte