Jean LENEUTRE
Directeur de thèse :
Patrick BELLOT
Groupe :
Génie Logiciel, Projet Logiques, Langages et
Spécifications
Laboratoire d'accueil :
Département Informatique, TELECOM Paris
Date de soutenance prévue :
janvier 1997
English version
Programmation par preuves : mise en oeuvre pour l'OMEGA Logique et
application au développement de programmes certifiés pour le domaine des
télécommunications.
Le problème consistant à savoir si un programme donné est correct,
c'est-à-dire vérifie bien certaines spécifications, est crucial en
informatique. La Logique Intuitionniste apporte une solution originale à ce
problème : grâce à l'isomorphisme de Curry-Howard (ou formule=type et
preuve=programme), on peut associer à toute démonstration un contenu
algorithmique. La construction d'un programme correct se fait alors selon
les trois étapes suivantes :
- spécification d'un objet informatique sous la forme d'une formule
logique ;
- démonstration logique de l'existence d'un tel objet (grâce à un système
d'aide à la démonstration) ;
- extraction du programme à partir de cette preuve.
L'objet de cette thèse concerne la mise en oeuvre de l'étape d'extraction
de programme pour une logique des actions (conçue au sein de notre équipe
et s'inspirant de la Logique Linéaire de J.-Y. Girard) et l'application au
développement de programmes certifiés pour le domaine des
télécommunications. Cette thèse se distingue des travaux existants par :
- une conception et une visée plus proche de l'informatique
que des mathématiques ;
- l'utilisation d'un formalisme logique ayant une puissance
d'expression plus forte ;
- la forme des programmes extraits : non typés,
impératifs ou récursifs.
Publications
1996
- (Bellot 96b)
P. BELLOT,
J-P. COTTIN,
A. DEMAILLE,
J. LENEUTRE,
E. ZARPAS,
"Démonstration automatique dans une logique des actions et de
la causalité" dans JSJ'96 Premières
Journées du
Séminaire Junior du LIPN "Intelligence Artificielle et Applications"
- (Bellot 96c)
P. BELLOT, J-P. COTTIN, J. LENEUTRE, B. ROBINET, E. ZARPAS,
"Prolegomena of a Logic of Causality and Dynamicity",
to appear in STUDIA LOGICA,
1996.
- (Bellot 96d)
P. BELLOT,
J-P. COTTIN,
A. DEMAILLE,
J. LENEUTRE,
E. ZARPAS,
"Automated deduction for protocols design"
in proceedings of Third Workshop on Automated Reasoning:
Bridging the Gap between Theory and Practice.
- (Bellot 96e)
P. BELLOT,
J-P. COTTIN,
A. DEMAILLE,
J. LENEUTRE,
E. ZARPAS,
"Using a logic of actions to design protocols"
in proceedings of the 5th open workshop on High speed Network, Télécom-Paris-
Universität Stuttgart, March 1996.
- (Bellot 96g)
P. BELLOT,
J-P. COTTIN,
A. DEMAILLE,
J. LENEUTRE,
E. ZARPAS,
"A Logic of Actions for Imperative Program Synthesis"
in proceedings of Logic Colloquium'96, LC'96,
J.M. Larrazabal ed.,
San Sebastian (Espagne), juillet 1996.
- (Bellot 96h)
P. BELLOT,
J-P. COTTIN,
A. DEMAILLE,
J. LENEUTRE,
E. ZARPAS,
"Création d'un environnement de génération de programmes utilisant
une logique des actions"
in Journées ADER, GDR Programmation, Paris (France), mai 1996.
- (Bellot 96f)
P. BELLOT,
J-P. COTTIN,
A. DEMAILLE,
J. LENEUTRE,
E. ZARPAS,
"Towards Bug Free Software Engineering for Telecommunication",
in proceeding of
The Eighth International Conference (Joint Europe-USA Conference) on ARTIFICIAL
INTELLIGENCE APPLICATIONS (EXPERSYS'96) ,
PARIS-MARNE LA VALLEE, France
(21 - 22 October 1996)
- (Cottin 96b)
J-P. COTTIN,
A. DEMAILLE,
J. LENEUTRE,
E. ZARPAS,
"Création d'un environnement de programmation
utilisant une logique des actions",
dans JDIR'96, Paris, Septembre 1996.
- (Bellot 96a)
P. BELLOT,
J-P. COTTIN,
A. DEMAILLE,
J. LENEUTRE,
E. ZARPAS,
"Logique et Synthèse de Programmes Impératifs"
dans Journées du GDR Programmation, C. Paulin-Mohring ed.,
Orléans
(France), novembre 1996.
1995
- (Bellot 95e)
P. BELLOT,
J-P. COTTIN,
J. LENEUTRE,
E. ZARPAS,
"Programmation par preuves avec une logique des actions", dans
Journées du GDR Programmation,
C. Paulin-Mohring ed.,
Grenoble (France), novembre 1995.
- (Bellot 95d)
P. BELLOT,
J-P. COTTIN,
J. LENEUTRE,
E. ZARPAS,
"Méthodes formelles et protocoles, proposition pour une logique
des actions et de la causalité", dans Actes des
8èmes Journées Internationales sur Le Génie Logiciel
et ses Applications, EC2 ed., pp. 267-280
Paris-La Défense (France),
novembre 1995.
- (Bellot 95h)
P. BELLOT,
J-P. COTTIN,
A. DEMAILLE,
J. LENEUTRE,
E. ZARPAS,
"Calcul et programmation dans une logique
des actions et de la causalité",
dans
Séminaire ENS/ENST
Modèles, Langages et Télécommunications,
B. Robinet ed., Paris, septembre 1995.
1994
- (Bellot 94a)
P. BELLOT,
J. LENEUTRE,
E. ZARPAS,
"The B-logic, from the Big Bang to the Big Crunch",
in
Logic Colloquiun'94, LC'94,
Clermont-Ferrand (France),
july 1994.
Published in the
Bulletin of Symbolic Logic,
vol. I, n. 2,
D. Richard ed., june 1995.
- (Bellot 94b)
P. BELLOT,
J. LENEUTRE,
B. ROBINET,
E. ZARPAS,
Future Trends of Software Engineering,
TELECOM Paris internal report n. 94D020,
Paris (France),
september 1994.
Email :
leneutre@inf.enst.fr
Page maintenue par Jean-Philippe COTTIN (cottin@inf.enst.fr)
et Patrick BELLOT (bellot@inf.enst.fr)
Jean LENEUTRE