Venez découvrir la théorie de la réécriture et ses applications

C’est en 2006, à Nancy, qu’a lieu la première École internationale en réécriture (International School of Rewriting ou ISR). Portée par la Fédération internationale d’informatique (IFIP) , cette école d’été est ensuite organisée par différents pays d’Europe et d’Amérique latine. En 2019, elle revient enfin en France, à Paris, grâce au travail d’Olivier Hermant (MINES ParisTech) et de Frédéric Blanqui (équipe Inria Deducteam, commune avec le Laboratoire Spécification et Vérification -LSV- et l’ENS Paris-Saclay). Ces deux familiers du domaine se sont répartis les tâches de logistique, de recherche de financement et de construction de programme, pour proposer une édition 2019 pleine de nouveautés.

L’ISR , qu’est-ce que c’est ?

L’ISR est une formation courte, d’une semaine, consacrée à la théorie de la réécriture , un modèle de calcul particulièrement important pour la programmation ou la démonstration de théorèmes . En remplaçant de proche en proche les termes d’une expression suivant des règles de transformation prédéterminées, la réécriture va permettre de reformuler un problème jusqu’à atteindre une solution. Cette approche nous est familière à tous quand elle touche les expressions algébriques simples. Souvenez-vous de (a+b)²= a²+2ab+b²… Mais la réécriture s’applique à tous types d’objets mathématiques et trouve ainsi des applications dans de très nombreux domaines , de la chimie organique à la vérification de logiciel, en passant par l’industrie ferroviaire.

Pour cette édition 2019 de l’ISR , le programme s’est allongé d’une journée. Destiné en priorité aux doctorants, il accueille aussi des étudiants de master qui bénéficient cette année d’un tarif préférentiel. Les chercheurs, jeunes ou confirmés, curieux des applications qui seront présentées, sont évidemment également les bienvenus.

 

Le système en deux parcours permet de se positionner comme une formation en deux ans.

 

 

Frédéric Blanqui.

Deux parcours au choix

Selon le format habituel de l’école, la cinquantaine de participants attendus à Paris se verra proposer deux parcours (tracks ) :

• Vous êtes débutant ? La track  "basique" est faite pour vous et pour tous ceux qui veulent apprendre les fondamentaux de la réécriture . Trois intervenants vont alterner cours et exercices pour vous transmettre les techniques de base de ce système. Avec, en fin de semaine, un examen optionnel pour les participants qui auraient des crédits ECTS à valider. Nouveauté de cette édition, une journée et demie consacrée au λ-calcul, utilisé par les langages de programmation.
• Vous connaissez déjà la réécriture ? La track  "avancée" vous permet d’approfondir vos connaissances et de découvrir de nouvelles applications . Le programme, qui comprend douze séances d’1h30, présentera des approches théoriques ou pratiques, des études de cas…

Parmi les thématiques sélectionnées par Olivier Hermant et Frédéric Blanqui pour renouveler ce cours avancé, figurent notamment :

• la modélisation des interactions moléculaires ;
• la représentation des processus quantiques ;
• l’application à la musicologie par informatique, et à la transcription du rythme.

Ceux qui s’inscriront à l’école d’été avant le 17 mai, bénéficieront d’une réduction de 20 %.

L’équipe Deducteam

• Fondation de l’équipe  : en 2013, Frédéric Blanqui rejoint Gilles Dowek, directeur de recherche Inria, qui menait des travaux exploratoires sur la vérification des preuves formelles.
• Localisation  : centre de recherche Inria Saclay – Île-de-France depuis le 1^er janvier 2016.
• Thème de recherche  : Deducteam travaille dans le monde des preuves formelles et de leur vérification. L’objectif est de développer un standard pour pouvoir vérifier sans ambiguïté la correction d’un programme ou d’un théorème mathématique. En particulier dans les domaines ferroviaire et aéronautique, où des logiciels sans erreur sont un prérequis essentiel pour assurer la sûreté et la sécurité de ces applications critiques.
• Principale réalisation  : Dedukti , un outil à l’architecture simple et modulaire, qui cherche à reproduire dans le domaine de la preuve ce que font les logiciels assembleurs en programmation : résoudre les problèmes d’interopérabilité entre systèmes de preuves différents pour permettre de combiner ces divers langages les uns avec les autres.
• Projet en cours  : Logipedia , un projet qui a pour objectif de traduire les librairies de preuves formelles développées par différentes équipes pour les agréger en une e-infrastructure européenne. La réunion de lancement s’est tenue fin janvier 2019, au Laboratoire Spécification et Vérification (LSV) d’Inria.