[Sim92] Des preuves de totalitÃ© de fonctions comme synthÃ¨se de programme

Mémoire de Thèse : Soutenue le: 01 January 1992, pp. 130, pp.: Directeur:
Rapporteur 1:
Rapporteur 2:
Membre du jury:
Membre du jury:
Membre du jury:, : Evidence of entire functions as program synthesis,

Auteurs: M. Simonot

motcle:

Résumé: LES TRAVAUX DE THEORIE DE LA DEMONSTRATION AXES SUR LE LAMBDA-CALCUL TYPE NOUS DONNENT LA POSSIBILITE DE CONSTRUIRE DES SYSTEMES DE SYNTHESE DE PROGRAMMES A PARTIR DE PREUVES FORMELLES DE SPECIFICATIONS. L'INTERET DES SYSTEMES DEVELOPPES DANS CE CONTEXTE EST QUE LES PROGRAMMES QUI Y SONT OBTENUS SONT CORRECTS. LES AUTEURS DE CETTE THESE UTILISENT UN SYSTEME DE LAMBDA-CALCUL TYPE DANS LEQUEL, POUR OBTENIR UN PROGRAMME QUI CALCULE UNE FONCTION, IL SUFFIT DE PROUVER QUE CELLE-CI EST TOTALE SUR SON DOMAINE. APRES AVOIR PRESENTE LE CADRE GENERAL DANS LEQUEL ILS TRAVAILLENT (LA THEORIE DE TYPES RECURSIFS), LES AUTEURS PROPOSENT UNE METHODE DE PREUVE PAR RECURRENCE POUR LES ENONCES DE TOTALITE DE FONCTIONS EQUATIONNELLEMENT DEFINIES. ILS DONNENT ENSUITE DEUX STRATEGIES AUTOMATIQUES DE RECHERCHE DE PREUVES CONFORMES A CETTE METHODE ET DEMONTRENT QUE TOUTES DEUX SONT CORRECTES ET COMPLETES. LA DIFFERENCE ESSENTIELLE ENTRE CES DEUX STRATEGIES EST LE PRINCIPE DE RECURRENCE UTILISE. AUTOUR DE CES STRATEGIES, LES AUTEURS ONT IMPLEMENTE UN SYSTEME DE PROGRAMMATION PAR PREUVE SE PRESENTANT COMME UN LANGAGE DE PROGRAMMATION FONCTIONNELLE

Equipe: sys

BibTeX

@phdthesis {
	Sim92,
	title	=	"{Des preuves de totalitÃ© de fonctions comme synthÃ¨se de programme}",
	author	=	"M. Simonot",
	year	=	1992,
	pages	=	"130",
	address	=	"{CEDRIC Laboratory, Paris, France}",
	note	=	"{ Directeur: Rapporteur 1: Rapporteur 2: Membre du jury: Membre du jury: Membre du jury:}",
}