[Caml-list] JFLA 2012

[Caml-list] JFLA 2012

[Damien Pous]

[ 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

[Caml-list] JFLA 2012

[Damien Pous]

(This message is intentionally written in French)

* MERCI DE FAIRE CIRCULER * MERCI DE FAIRE CIRCULER * MERCI DE FAIRE CIRCULER *

         APPEL A PARTICIPATION           APPEL A PARTICIPATION

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

              Journées Francophones des Langages Applicatifs
                       Organisées par l'INRIA

                       4 février au 7 février 2012

JFLA'2012 est la vingt troisième conférence francophone
organisée autour des langages applicatifs et des techniques de certification
basées sur la démonstration.

Ces nouvelles journées se tiendront du

           4 février au 7 février 2012.

Elles auront lieu à la mer, à

           Carnac, à proximité de Lorient, Rennes.

Toujours centrée sur l'approche fonctionnelle de la programmation, la
conférence porte également sur les techniques et outils complémentaires qui
élèvent le niveau de qualité des logiciels (systèmes d'aide à la preuve,
réécriture, tests, démonstration automatique, vérification).

Les JFLA réunissent concepteurs et utilisateurs dans un cadre
agréable qui facilite la communication; ces journées ont pour ambition de
couvrir le domaine des langages applicatifs au sens large, en y incluant les
apports d'outils d'autres domaines qui permettent la construction de systèmes
logiciels plus sûrs. L'enseignement de l'approche fonctionnelle du
développement logiciel (spécification, sémantiques, programmation,
compilation, certification) est également un sujet qui concerne au plus haut
point les JFLA.

C'est pourquoi des contributions sur les thèmes suivants sont
particulièrement recherchées (liste non exclusive) :

- Langages fonctionnels et applicatifs : sémantique, compilation, optimisation,
 mesures, tests, extensions par d'autres paradigmes de programmation.

- Spécification, prototypage, développements formels d'algorithmes.

- Utilisation industrielle des langages fonctionnels et applicatifs.

- Assistants de preuve : implémentation, nouvelles tactiques,
 développements présentant un intérêt technique ou méthodologique.

- Enseignement dans ses aspects liés à l'approche fonctionnelle
 du développement.

Inscriptions
------------

 Avant le 20 janvier : http://registration.net-resa.com/site/675

Orateurs invités
----------------
 Benjamin Grégoire (Sophia Antipolis)
 Dimitrios Vytiniotis (Microsoft Research)


Cours
-----
 Jean-Christophe Filliâtre (CNRS)
 Matthieu Sozeau (INRIA Paris -- Rocquencourt)

Comité de programme
-------------------
       Assia Mahboubi, Présidente (INRIA Saclay -- Île-de-France)

       Damien Pous, Vice président (CNRS)

       David Baelde (Universtié Paris Sud 11)

       Fréderic Besson (INRIA Rennes -- Bretagne Atlantique)

       Sandrine Blazy (Université Rennes 1)

       Louis Mandel (Université Paris Sud 11)

       Guillaume Melquiond (INRIA Saclay -- Île-de-France)

       Julien Narboux (Université de Strasbourg)

       Yann Régis-Gianas (Université Paris 7)

       Christine Tasson (Université Paris 7)

Dates importantes
-----------------
23 octobre 2011 : Date limite de soumission
18 novembre 2011 : Notification aux auteurs
9 décembre 2011 : Remise des articles définitifs
20 janvier 2012 : Date limite d'inscription aux journées
4 février au 7 février 2012 : Journées

Pour tout renseignement d'ordre administratif, contacter
--------------------------------------------------------
Chantal Girodon
INRIA Service IST
 Domaine de Voluceau - BP 105
 78153 Le Chesnay cedex - France
Tel : +33 (0)1 39 63 50 53 - Fax : +33 (0)1 39 63 56 38
email : symposia@inria.fr

http://jfla.inria.fr/2012/

[Caml-list] JFLA'2012

[Damien Pous]

(This message is intentionally written in French)

* MERCI DE FAIRE CIRCULER * MERCI DE FAIRE CIRCULER * MERCI DE FAIRE CIRCULER *

PREMIER APPEL AUX COMMUNICATIONS       PREMIER APPEL AUX COMMUNICATIONS

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

              Journées Francophones des Langages Applicatifs
                       Organisées par l'INRIA

                       4 février au 7 février 2012

JFLA'2012 est la vingt troisième conférence francophone
organisée autour des langages applicatifs et des techniques de certification
basées sur la démonstration.

Ces nouvelles journées se tiendront du

           4 février au 7 février 2012.

Elles auront lieu à la mer.

Toujours centrée sur l'approche fonctionnelle de la programmation, la
conférence porte également sur les techniques et outils complémentaires qui
élèvent le niveau de qualité des logiciels (systèmes d'aide à la preuve,
réécriture, tests, démonstration automatique, vérification).

Les JFLA réunissent concepteurs et utilisateurs dans un cadre
agréable qui facilite la communication; ces journées ont pour ambition de
couvrir le domaine des langages applicatifs au sens large, en y incluant les
apports d'outils d'autres domaines qui permettent la construction de systèmes
logiciels plus sûrs. L'enseignement de l'approche fonctionnelle du
développement logiciel (spécification, sémantiques, programmation,
compilation, certification) est également un sujet qui concerne au plus haut
point les JFLA.

C'est pourquoi des contributions sur les thèmes suivants sont
particulièrement recherchées (liste non exclusive) :

- Langages fonctionnels et applicatifs : sémantique, compilation, optimisation,
 mesures, tests, extensions par d'autres paradigmes de programmation.

- Spécification, prototypage, développements formels d'algorithmes.

- Utilisation industrielle des langages fonctionnels et applicatifs.

- Assistants de preuve : implémentation, nouvelles tactiques,
 développements présentant un intérêt technique ou méthodologique.

- Enseignement dans ses aspects liés à l'approche fonctionnelle
 du développement.

Les JFLA cherchent avant tout des articles de recherche
originaux qui apportent une réelle nouveauté. Toutefois, un article traitant
d'un sujet qui intéresse plusieurs disciplines sera examiné avec soin, même
s'il a préalablement été présenté à une autre communauté sans rapport avec
celle des JFLA.  Un article ayant été traduit en français à
partir d'une publication récente en anglais sera examiné, à condition que la
traduction apporte un élément nouveau.

Les articles soumis aux JFLA sont relus par au moins 2 personnes
s'ils sont acceptés, 3 personnes s'ils sont rejetés.

Les critiques des relecteurs sont toujours bienveillantes et la plupart du
temps encourageantes et constructives, même en cas de rejet.

Il n'y a donc pas de raison de ne pas soumettre aux JFLA !

Orateurs invités
----------------
 Dimitrios Vytiniotis (Microsoft Research).
 (Non communiqué) ((Non communiqué)).


Cours
-----
 Jean-Christophe Filliâtre (CNRS).
 Matthieu Sozeau (INRIA Paris -- Rocquencourt).

Comité de programme
-------------------
       Assia Mahboubi, Présidente (INRIA Saclay -- Île-de-France)

       Damien Pous, Vice président (CNRS)

       David Baelde (Universtié Paris Sud 11)

       Fréderic Besson (INRIA Rennes -- Bretagne Atlantique)

       Sandrine Blazy (Université Rennes 1)

       Louis Mandel (Université Paris Sud 11)

       Guillaume Melquiond (INRIA Saclay -- Île-de-France)

       Julien Narboux (Université de Strasbourg)

       Yann Régis-Gianas (Université Paris 7)

       Christine Tasson (Université Paris 7)

Soumission
----------
Date limite de soumission : 16 octobre 2011

Les actes des jfla seront remis aux participants durant la conférence.

Les soumissions doivent être soit rédigées en français, soit présentées en
français. Elles sont limitées à 15 pages A4. Le style latex est imposé et se
trouve sur le site WEB des journées à l'adresse suivante :

        http://jfla.inria.fr/2012/actes.sty

La soumission est uniquement électronique, selon la méthode détaillée dans

        http://jfla.inria.fr/2012/instructions.fr.html

La soumission doit être réalisée à l'aide du système EasyChair

         http://www.easychair.org/conferences/?conf=jfla2012


Dates importantes
-----------------
16 octobre 2011 : Date limite de soumission
18 novembre 2011 : Notification aux auteurs
9 décembre 2011 : Remise des articles définitifs
20 janvier 2012 : Date limite d'inscription aux journées
4 février au 7 février 2012 : Journées

Pour tout renseignement d'ordre administratif, contacter
--------------------------------------------------------
Chantal Girodon
INRIA Service IST
 Domaine de Voluceau - BP 105
 78153 Le Chesnay cedex - France
Tel : +33 (0)1 39 63 50 53 - Fax : +33 (0)1 39 63 56 38
email : symposia@inria.fr

http://jfla.inria.fr/2012/