Abstract FR:

A partir d'une étude systématique de la construction de preuves en logique linéaire, il s'agit de définir un modèle de programmation parallèle qui repose sur cette notion comme principe de calcul. La logique linéaire étant définie par un calcul des séquents, la propriété de permutabilité d'inférences constitue la base d'une forme particulière de normalisation des preuves en vue de leur construction automatique tant en chainage avant qu'en chainage arrière. Cela permet ensuite d'interpréter cette construction de preuves comme un modèle du calcul parallèle dans un fragment particulier de la logique linéaire intuitionniste. Ce modèle permet de donner une représentation logique de concepts de base du parallélisme (communication synchrone et asynchrone, indéterminisme, interface, implantation d'une spécification).