Formalisation des langages concurrents et à objets
modulo l'alpha-conversion
Guillaume Gillard
Projet Certilab, INRIA Sophia, France
Juin 19, 11h, E006
Abstract:
La fiabilité et la robustesse des programmes deviennent chaque jour des enjeux plus importants. Les techniques de la preuve assistée par ordinateur proposent une solution prometteuse à ces problèmes même si aujourd'hui le champ d'application de ces méthodes est encore limité. L'étude formelle des langages de programmation est un domaine où l'utilisation de ces méthodes semble particulièrement prometteuse. Dans ce domaine, la maîtrise des lieurs d'un langage et des problèmes d'alpha conversion qui s'y rattachent sont des pré requis indispensables avant l'étude de propriétés du langage comme, par exemple, ses sémantiques dynamique et statique. Pour le moment, aucune des différentes possibilités connues de formalisation dans des systèmes tels que Coq de ces notions ne sont pleinement satisfaisantes. Notre travail consiste à montrer comment il est possible d'adapter une méthode qui mélange indices de Bruijn et noms aux langages de programmation ainsi qu'aux prédicats définis sur ces langages. Au travers de deux langages concurrents dont l'un est orienté objet nous verrons comment il est possible, en partant de formalismes de Bruijn, de réintroduire des noms dans les lieurs. Nous montrerons que cette méthode permet d'obtenir des principes d'induction pour les termes et les prédicats sur ces langages (relation de transition et système de types) qui internalisent l'alpha-conversion dans le système Coq. Enfin, pour permettre à chacun de se faire son idée quand à l'efficacité de cette méthode nous la comparons avec une méthode de Bruijn classique et une méthode inspirée des téchniques développées par J. McKinna et R. Pollack.
Fiability and robustness have turned into central issues for computer
programs. Computer
assisted proof is a technique that offers a promising solution to this
problem, even if the
range of applications of these methods is still limited.
However, one field that is particularly suited to these methods is the
formal study of
programming languages. In this field, mastering the binder and
the corresponding
alpha conversion problems is a necessary prerequisite before studying
the language
properties such as its dynamical and statical semantics.
So far, no existing method offer a fully satisfactory formalisation of
such concepts in
systems like Coq. Our work consist in showing how it is possible to take
a method that mix De
Brujin indices and names for formalizing the binders of the programming
languages.
Through two concurrent languages, one of which is object oriented, we
will see how it is
possible to reintroduce names in binders and relay the de Bruijn indices we started with beyond the scene.
We will show
that this method provides us with induction principles for the terms and
predicates of those
languages (transition relation and type system) that internalize
alpha-conversion in the Coq
system. Lastly, to allow the reader to form his/her own opinion on the
efficiency of this
method, we compare our encodingd with a classical de Brujin encoding and with another encoding using a
method developped by
J. McKinna and R. Pollack.
Back to schedule.
Nicolas Magaud
Last modified: Tue Jun 12 14:08:27 MEST 2001