[Caml-list] JFLA 2012

[Damien Pous <Damien.Pous@inria.fr>]

[ This message is intentionally written in French ]

                        Ultime appel à participation

                    JFLA'2012 (http://jfla.inria.fr/2012/)

                Journées Francophones des Langages Applicatifs
                   4 février au 7 février 2012, Carnac


Vous pouvez encore vous inscrire aux JFLA 2012 jusqu'à demain! La page
d'inscription est disponible sur le site http://jfla.inria.fr/2012/.

L'édition 2012 des Journées Francophones des Langages Applicatifs aura lieu à
Carnac du 4 février à 15h au 7 février 2012 à midi. Pour tout renseignement,
contacter symposia@inria.fr.

Les journées des 4 et 5 février seront consacrés aux cours invités de
Jean-Christophe Filliâtre (LRI, Cnrs) et Matthieu Sozeau (Inria). Les journées
des 6 et 7 février seront consacrés aux exposés présentant les articles
sélectionnes ainsi qu'aux exposés des orateurs invités Benjamin Grégoire (Inria)
et Dimitrios Vytiniotis (Microsoft Research).

La liste des articles acceptés est disponible ici:
http://jfla.inria.fr/articles_acceptes_2012.html

A bientôt à Carnac,

Assia Mahboubi et Damien Pous


*Cours Invités*


Jean-Christophe Filliâtre : Vérification déductive de programmes avec Why3

Ce cours est une introduction à la preuve de programmes en général, et à l'outil
Why3 en particulier (http://why3.lri.fr/). L'outil Why3 permet d'écrire des
programmes dans un langage très proche d'OCaml (polymorphisme, types
algébriques, filtrage, exceptions, références, tableaux, etc.), de leur donner
une spécification dans une logique du premier ordre, et de prouver leur
correction à l'aide de démonstrateurs interactifs ou automatiques (Coq,
Alt-Ergo, Z3, CVC3, etc.). Au travers de nombreux exemples, ce cours introduit
des concepts élémentaires de preuve de programmes (pré- et postcondition,
invariant de boucle, variant) mais aussi des techniques (spécification, preuve
de terminaison, modélisation de structures de données).


Matthieu Sozeau : Classes de types en Coq

Nous présentons dans ce cours une extension légère à Coq permettant de faire des
développements génériques via un mécanisme de surcharge inspiré d’Haskell. Sans
modifier le langage primitif du calcul des constructions, les classes donnent à
l’utilisateur des facilités de haut niveau pour travailler avec des structures
abstraites tout en permettant leur instanciation efficace sur des structures
concrètes. Il permet aussi d’ajouter de l’intelligence au système en étendant
l’algorithme de typage, lui permettant de trouver par résolution un habitant
d’une classe donnée. Ce principe de surchage s’étend naturellement à
l’environnement tout entier, en particulier au système de tactiques de Coq. Nous
présenterons tout d’abord le fonctionnement basique du système de classes
implémenté dans Coq (et disponible depuis la version 8.2) puis son utilisation
pratique au cours d’un tutoriel. Nous introduirons progressivement différents
raffinements rendant le système plus agréable à l’usage.


*Exposés Invités*

Benjamin Grégoire : Easycrypt : un outil pour les preuves de
cryptographie exacte

Après une rapide introduction des notions de cryptographie exacte,
je présenterai la notion de preuve par réduction qui est une méthodologie
couramment utilisée par les cryptographes pour établir la
correction et la sécurité de primitives cryptographiques telles que
Elgamal ou OAEP.
Je présenterai ensuite les différentes notions qui ont permis
de développer Certicrypt (une librairie Coq permettant de formaliser
la sécurité de primitives cryptographiques), en mettant un
accent particulier sur la logique pRHL (probabilistic Relationnal Hoare Logic).
J'illustrerai ensuite ces notions sur un exemple simple :
 la sécurité sémantique de Elgamal.
Je finirais l'exposé avec la présentation d'un nouvel outil (Easycrypt)
qui réutilise les concepts mis en place dans Certicrypt mais
repose sur une utilisation intensive de prouveurs
automatiques tels que alt-ergo, z3, ou vampire.


Dimitrios Vytiniotis : Stop when you are Almost-Full: terminator and size-change
termination in Coq

[joint work with Thierry Coquand]
Disjunctive well-foundedness (as used for instance in the Terminator tools),
size-change termination, and well-quasi-orders (used in term-rewrite systems)
are examples of techniques that have been successfully applied to automatic
proofs of program termination and online termination testing, respectively.
Although these works originate in different communities, there is an intimate
connection between them - they rely on closely related principles and employ
similar arguments from Ramsey theory. At the same timethere is a notable absence
of these techniques in programming systems based on constructive type theory.
In this talk we will explain the aforementioned connection and present some
novel tools to perform induction in Coq, inspired from  that large body of
previous work. The benefit is nice composability properties of termination
arguments at the cost of intuitive and  lightweight user obligations.
Inevitably, we have to present some Ramsey-like arguments: Though similar proofs
are typically classical, we offer an entirely constructive development standing
on the shoulders of Veldman and Bezem, and Richman and Stolzenberg. This work is
to our knowledge the first constructive justification of Terminator and
Size-Change termination and opens the way towards employing these techniques,
without any further logical assumptions, in Coq.


*Articles acceptés*

Simon Boulier et Alan Schmitt : Formalisation de HOCore en Coq

Pierre Boutillier : Ad hoc reductions make structural guard condition stricter
and smarter

Cyril Cohen : Construction des nombres algébriques réels en Coq

Christophe Deleuze : Concurrence et continuations en OCaml

Jean-François Durfourd : Dérivation de l'algorithme de Schorr-Waite en Coq par
une méthode algébrique

Fabrice Le Fessant et Thomas Gazagnaire : Gestion de projet avec ocp-build

Mathieu Jaume et Renaud Rioboo : Développement de systèmes sécurisés avec
l'atelier FoCaLiZe

Catherine Lelay et Guillaume Melquiond : Différentiabilité et intégrabilité en
Coq. Application à la formule de d'Alembert

Daniel De Rauglaudre : Vérification formelle de conditions d'ordonnancabilité de
tâches temps réel périodiques strictes

Bernard Serpette et Emmanuel Chailloux : Séparation des couleurs dans un
lambda-calcul bichrome