Proposition de stage
Formalisation d'une logique pour
raisonner sur des programmes impératifs d'ordre supérieur
1 Lieu
Laboratoire de Recherche en Informatique
UMR 8623 du CNRS
Bât. 490, Université Paris Sud
91405 Orsay cedex
2 Personnes encadrant le stage
3 Titre : Formalisation d'une logique pour
raisonner sur des programmes impératifs d'ordre supérieur
3.1 Résumé
Il est difficile de spécifier et de raisonner sur des programmes qui
combinent des fonctions d'ordre supérieur et des traits impératifs
comme les structures mutables.
Cependant ces traits de programmation sont au coeur d'un langage de
programmation tel que Ocaml et pouvoir les traiter est une étape
essentielle vers le développement de bibliothèques de programmes
certifiés.
M. Berger, K. Honda et N. Yoshida ont proposé dans des articles
récents une méthode d'analyse de programmes qui repose sur des
techniques de preuve développées pour le p-calcul et se présente
comme une généralisation de la logique de Hoare permettant de prendre
en compte les fonctions d'ordre supérieur, des références modifiables
en place et de possibles alias.
Des propriétes de validité et de complétude ont été prouvées pour
cette logique, cependant il n'existe pas actuellement d'environnement
permettant de mécaniser le raisonnement sur les programmes en
utilisant cette logique.
L'objectif du stage est d'étudier la formalisation dans l'assistant de
preuve Coq d'un fragment de cette logique. On pourra commencer par la
partie élémentaire concernant les fonctions d'ordre supérieur et les
références sans alias. L'objectif est double, il s'agit à la fois de
consolider l'étude des propriétés meta-théoriques de ce calcul et
d'offrir un environnement minimal pour étudier mécaniquement des
exemples élémentaires. À plus long terme, cette étude peut servir de base au
développement d'un environnement pour le raisonnement sur les
programmes fonctionnels avec effets de bord.
3.2 Déroulement
Le stage débutera par l'étude des articles sur la logique à implanter
et par l'identification du noyau à étudier.
La formalisation dans l'assistant Coq pourra s'appuyer sur des
modélisations de logique de Hoare réalisées dans l'assistant Isabelle/HOL.
Ce travail s'inscrit dans l'action coordonnée européenne
http://www.cs.chalmers.se/Cs/Research/Logic/Types/TYPES,
elle pourra donner lieu à des échanges avec le groupe autour de
Martin Berger à Queen Mary, university of London.
3.3 Prérequis
Une connaissance de base des langages de
programmation fonctionnels et de la logique ainsi qu'une
expérience préalable à la modélisation dans l'assistant de preuve Coq
sont recommandées.
References
- [1]
-
Martin Berger, Kohei Honda, and Nobuko Yoshida.
A Logical Analysis of Aliasing in Imperative Higher-Order
Functions.
In ICFP, 2005.
http://www.dcs.qmul.ac.uk/~kohei/logics/.
- [2]
-
Martin Berger, Kohei Honda, and Nobuko Yoshida.
An Observationally Complete Program Logic for Imperative
Higher-Order Functions.
In LICS, 2005.
http://www.dcs.qmul.ac.uk/~kohei/logics/.
This document was translated from LATEX by
HEVEA.