Université Lille1 - Sciences et Technologies Types de données et récurrence bien fondée dans un système de programmation par preuves 005.1 Ordinateurs Programmation Langages formels Text Electronic Thesis or Dissertation fr 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 application/pdf 1 : 1 Mo https://pepite-depot.univ-lille.fr/LIBRE/Th_Num/1990/50376-1990-93.pdf Bezzazi El-Hassan 1900-01-01 134492153 1990LIL10140 1990-01-01 Informatique Université Lille1 - Sciences et Technologies 026404184 Doctorat non oui Werner G. ddc:000 ASCII PDF 9999