Concurrent constraint programming and linear logic
Résumé
In this thesis, we study the close links between linear logic and on current constraint programming, from the angle of semantics and more precisely of program verification.
We refine the observables that can be characterized in linear logic and extend existing results to obtain a more precise and more general semantics. These results are only based on a more faithful translation
from agents into logic formulae and on an enrichment of the theory. We also present an original method to get program proofs, based on the provability semantics of linear logic: phase semantics. This gives us a tool for verification, enjoying lots of good properties, like the ability to prove a universal property of the program simply with
a counter-example; an easy abstraction from the program; and the simplicity of the proofs obtained.
We thus construct a systematic method of proof generation and after applying it to classical examples, we study its automatization. This research leads to the implementation of a prototype-prover which can live side by side with our interpreter for linear concurrent constraint languages.