Observational equivalences for linear logic CC languages

TL;DR

This paper develops observational equivalences for linear logic-based concurrent constraint programming (LCC), connecting it with process algebras and classical constraint languages, and providing a formal semantics framework.

Contribution

It introduces a structural operational semantics for LCC, explores observational equivalences, and relates LCC to the asynchronous -calculus and classical constraint languages.

Findings

LCC can be semantically characterized using a label transition system.

Observational equivalences in LCC can be adapted to classical constraint languages.

Asynchronous -calculus can be represented as restrictions of LCC.

Abstract

Linear logic Concurrent Constraint programming (LCC) is an extension of concurrent constraint programming (CC) where the constraint system is based on Girard's linear logic instead of the classical logic. In this paper we address the problem of program equivalence for this programming framework. For this purpose, we present a structural operational semantics for LCC based on a label transition system and investigate different notions of observational equivalences inspired by the state of art of process algebras. Then, we demonstrate that the asynchronous \pi-calculus can be viewed as simple syntactical restrictions of LCC. Finally we show LCC observational equivalences can be transposed straightforwardly to classical Concurrent Constraint languages and Constraint Handling Rules, and investigate the resulting equivalences.