Abstract FR:

Nous etudions des connections entre la logique et la programmation concurrente par contraintes (cc) dans le paradigme programme = formule et calcul = recherche de preuve qui est celui de la programmation logique, et nous montrons que la logique intuitionniste et la logique lineaire permettent de caracteriser certaines observations interessantes du comportement operationnel des programmes (stores, succes), mais ne rendent pas bien compte des phenomenes de synchronisation. Cela nous amene a introduire une version mixte de la logique lineaire, combinant des connecteurs commutatifs et des connecteurs non-commutatifs. Nous la presentons par un calcul des sequents classique (qui etend d'une part la logique lineaire commutative et d'autre part la logique lineaire non-commutative cyclique) et par les elements de base d'une theorie de la demonstration : une semantique des phases et l'elimination des coupures. La logique lineaire mixte permet de caracteriser des observations fines : les suspensions d'un agent cc.