Claude Marché -Preuve de programmes C et
Java par traduction fonctionnelle Résumé :
L'approche Why pour la preuve de programmes impératifs
consiste à traduire les programmes (annotés par des
spécifications) en
des programmes fonctionnels avec types dépendants. L'outil Why
qui
implémente cette approche produit, à partir d'un
programme annoté dans
son langage spécifique, un terme Coq équivalent, avec des
trous qui sont
les obligations de preuve nécessaire pour établir la
correction de ce
programme. Nous expliquons ce mécanisme, puis nous l'appliquons
pour
des programmes écrit en langage C ou Java. Nous expliquons la
modélisation nécessaire du tas mémoire, pour
parvenir à traiter les
programmes avec pointeurs et leur aliasing potentiel.
Silvio
Ranise - An Extensible and
Decidable Logic for
Pointer Programs
Manipulating Linked Lists Résumé :
When verifying C or Java programs, it is necessary to reason about
pointer-based data structures such as linked lists or binary trees.
In this talk, we introduce a theory of Linked Lists (LL, for
short) in many-sorted logic (with equality) that
allows us to express properties of programs manipulating linked lists.
We show that LL is decidable and that its satisfiability
problem is NP-complete. Furthermore, we show how LL can be
extended
to cope with arbitrary theories of scalar values which can be stored in
the lists by using a recent combination schema.
To show the practical usability of LL, we discuss program
annotations which allows us to verify the (partial) correctness of a
some programs manipulating linked lists. Finally, we discuss related
work
and issues related to an efficient implementation of the procedure.
Nicolas Peltier - Logique et
termes-graphes.
Résumé :
Nous proposons une logique clausale permettant de raisonner sur des
"termes-graphes", c'est-à-dire sur des termes "cycliques" avec
partage de structure. Les termes-graphes permettent de modéliser
d'une manière très naturelle des structures de
données communément utilisées -- telles que les
listes circulaires ou les listes doublement chaînées --
qui ne peuvent être exprimées naturellement par des termes
classiques (sauf au prix d'un codage coûteux en
efficacité).
Notre objectif est d'exprimer des algorithmes de transformations sur
ces termes-graphes et de raisonner sur leurs propriétés
(par exemple de prouver leur correction).
Nous définissons une logique pour ces termes-graphes,
fondée sur une relation de simulation comme unique symbole de
prédicat. Ces termes-graphes sont vus comme la
représentation de termes infinis, par conséquent deux
graphes bisimilaires seront considérés comme
équivalents.
Le problème de la satisfaisabilité est indécidable
(non semi-décidable) pour cette logique, mais nous proposons
un ensemble de règles d'inférences similaires aux
règles usuelles de paramodulation. Nous illustrons leurs
possibilités sur certains exemples simples.
Nous concluons en donnant quelques voix de recherche futures.
Karim Nour - Une logique
combinatoire classique Résumé :
On sait que la logique combinatoire (i.e. les termes obtenus par
application à partir des variables et des combinateurs S et K)
est équivalente au lambda calcul, que ce soit en version non
typée ou dans un calcul simplement typé (i.e. les types
sont obtenus
à partir de types atomiques et de la flèche). Ces
systèmes correspondent, en ce qui concerne les preuves, à
de la logique intuitionniste.
Nous étendons cette équivalence à la logique
classique. Nous présenterons une logique combinatoire
typée où les types sont ceux de
lambda_sym, le calcul symétrique de Barbanera et Berardi (i.e.
les types sont obtenus à partir du "et" du "ou" et de la
négation) et
montrerons son équivalence avec lambda_sym.
Claude
Kirchner et Benjamin Wack
-
Aspects sémantiques et
logiques du calcul de
réécriture
Résumé :
Le calcul de réécriture est un formalisme qui
intègre les mécanismes fonctionnels du lambda-calcul et
les capacités de filtrage de la réécriture. Il a
été introduit et utilisé à des fins
sémantiques et logiques, et permet de décrire la
sémantique de langages à base de règles comme de
paradigmes orientés objets. Nous présenterons notamment
les applications du calcul de réécriture à la
logique, en lien avec la déduction modulo.
René
David - Forte normalisation
de divers systemes de
lambda-calcul Résumé :
Il y a quelques années j'avais donné une preuve
très courte (1/2 page) de la forte normalisation du lambda
calcul simplement typé. Depuis, j'ai étendu cette preuve
à diverses extensions de ce calcul. Cela donne des preuves
formalisables dans l'arithmétique de Peano alors les
preuves existantes (il n'y en avait pas toujours) sortaient de ce
cadre.
La plupart des preuves de forte normalisation de systemes de reecriture
sont ou bien "sémantiques" (candidats de
réductibilité, ...) et sortent alors du cadre de
l'arithmétique ou bien basées sur des ordres intelligents
(recursive path ordering, ...).
Dans cet exposé, je donnerai les idées de base des
techniques que j'utilise : au lieu de trouver des ordres intelligents,
on met des ordres "simples" mais on choisit intelligemment les
étapes du calcul ou il y a décroissance.
Frédéric Prost
- Réécriture de
graphes. Résumé :
La réécriture de
graphes est un domaine largement moins exploré que celui de la réécriture de termes.
Pourtant par la manipulation directe d'arêtes (que l'on peut voir comme des pointeurs) la
réécriture de graphes permet d'exprimer des algortihmes efficaces et largements
utilisés dans la pratique, ce que ne permet pas la réécriture de
termes (même si, bien sûr, la réécriture de
termes permet de simuler ces
algorithmes). La réécriture de graphes permet aussi un traitement naturel des structures de
données cycliques alors que la réécriture de termes, par définition, ne
traite que des arbres. Nous présenterons un
nouveau cadre catégorique pour formaliser la
réécriture de
graphes. La réécriture sera vue comme un double pushout
dans la catégorie des
graphes étiquetés. Nous nous attacherons notamment
à montrer comment deux mécanismes
particuliers sont représentés : les réorientations
locales (rediriger un
pointeur précis) et globales (rediriger tous les pointeurs vers
un nouveau noeud).
Caroline Priou -
Séparabilité dans un
lambda calcul
non-déterministe
Résumé :
Ce travail est basé sur un article de U. de'Liguoro et A.
Piperno, notamment sur une extension du lambda calcul non typé
standard auquel nous rajoutons un opérateur de choix + et une
réduction non-déterministe associée. Nous
explorerons la sémantique opérationnelle de ce calcul, en
étendant la notion d'arbre de Böhm et d'approximant, et en
étudiant la convergence de type "must" des termes. Je
présenterai brièvement quelques techniques syntaxiques et
un premier résultat de semi-séparabilité. Enfin la
séparabilité est démontrable en
interprétant les termes dans des espaces sémantiques de
type D-infini aux propriétés appropriées et pour
lesquels nous avons complétude et adéquation.
Pierre
Lescanne -
Implantation de la logique de la
connaissance en COQ Résumé :
La logique épistémique est la logique de "Alice sait
que". La logique de la connaissance est celle de "tout le monde sait
parfaitement que" ou encore "Alice sait que Bob sait qu'Alice sait
que". Pour bien l'exprimer il faut un point fixe. Dans cet
exposé je raconterai des expériences que j'ai conduites
en COQ à la recherche de la meilleure formalisation, notamment
pour les puzzles que l'on y rencontre.
Renaud Rioboo - Le projet
Focal Résumé :
L'exposé présente l'atelier FoCaL basé sur
un langage de programmation permettant de développer dans un
cadre unifié aussi bien des algorithmes queleur spécification et
leur correction. Les sources FoCaL sont analyséesstatiquement puis traduites
en Ocaml pour être exécutées et en Coq pour
êtrevérifiées. Nous présenterons les concepts de base de FoCaL que sont
les entités, lescollections
et les espèces qui sont des analogues aux
éléments, ensembles et structures algébriques en
mathématiques. Nous illustrerons ces concepts à l'aide d'outils de
dévoloppement réalisés ausein de l'atelier et qui ont
permis de développer la librairie demathématiques
effectives du langage. Nous présenterons également Zenon le planificateur
de preuve de FoCaL quipermet
de réaliser des preuves avec une approche originale
adaptée auxmathématiciens.
Ces preuves sont ensuite traduites en Coq pour être
validées.
Olivier
Ruatta - Mathemagix
Résumé :
Nous présenterons le logiciel mathemagix. Tout d'abord les
paradigmes sur lesquels le logiciel est basé et le contexte dans
lequel il est développé (notamment les relations avec
Synaps et Mmxlib d'une part et TeXmacs d'autre part). Son objectif est
de fournir uniquement une couche langage/interpréteur de type
CAS générale en utilisant des bibliothèques
extérieures pour les structures de données et les
algorithmes. Nous montrerons comment étendre le logiciel avec
des bibliothèques extérieures (pour l'instant uniquement
en C/C++).
Jean-Guillaume Dumas -
Modélisation de la librairie
d'algèbre linéaire
LinBox Résumé :
Nous proposons un nouveau langage de modélisation
diagrammatique, DML. Le paradigme utilisé est celui de la
théorie des catégories et en particulier des
``pushouts''. Nous montrons que la plupart des structures
orientées objet peuvent être décrites avec cet
outil et proposons de nombreux exemples en C++, de l'héritage et
du polymorphisme à la généricité par
``templates''. Par ailleurs, la bibliothèque C++
d'algèbre linéaire LinBox a été
conçue pour allier efficacité et
généricité. Elle requiert donc de nombreuses
structures ``template'' et polymorphes. Grâce à DML, nous
proposons une description simple des structures complexes de cette
bibliothèque.
Pierre
Lescanne - Le calcul X en collaboration avec Stéphane Lengrand, Steffen van
Bakel et Dragisa Zunic Résumé :
Dans cet exposé, je voudrais présenter un langage
baptisé X, qui se fonde essentiellement sur le concept de
connexion; les entités de base y sont les "plugs" et les
"sockets". Dans X, conçu en collaboration avec Steffen van Bakel
et Stéphane Lengrand, on explique comment simplifier des
expressions décrivant de connexions, ainsi que beaucoup d'autres
choses. Derrière X, se cachent Curry, Howard et de Bruijn que
j'essaierai de démasquer.
Stéphane Lengrand
- Elimination des coupures et
normalisation en logique intuitioniste.
Résumé :
Le calcul des séquents LJ peut être vu comme le
système de typage d'une syntaxe de termes, et on décrit
diverses procédures d'élimination des coupures comme des
systèmes de réécriture sur les termes.
Les paires critiques ont une forme particulière qui peut se
résoudre selon deux stratégies: Appel par Nom et Appel
par Valeur.
Deux restrictions sur les règles de typage
génèrent respectivement deux fragments de LJ logiquement
complets: LJT et LJQ, qui sont respectivement stables par les
stratégies sus-mentionnées.
On fait ensuite le lien avec la déduction naturelle au travers
d'un calcul d'Espirito Santo étendant le lambda-calcul
simplement typé et isomorphe à LJ, et on y identifie les
fragments correspondants à LJT et LJQ. Le premier est isomorphe
au lambda-calcul alors que le deuxième correspond à un
calcul de Moggi adéquat pour l'Appel par Valeur et d'inspiration
monadique.
On montre ensuite comment restreindre encore plus LJQ tout en
conservant la complétude logique mais en perdant la
complétude calculatoire (tous les entiers non-nuls de Church se
réduisent sur 1), la taille des habitants d'un type étant
alors borné.
