A LINEAR LOGIC VIEW OF GAMMA STYLE COMPUTATIONS AS PROOF SEARCHES
Paola Bruscoli, Alessio Guglielmi · 1996
Using the methodology of abstract logic programming in linear logic, we establish a correct and complete translation between the language Nabla and first order linear logic. Nabla is a modification of the coordination language Gamma with parallel and sequential composition. Nabla, without modifying Gamma basic computational model, is amenable to this kind of analysis, at the price of a weaker expressive power. The translation is correct and complete in the sense that we establish a two way correspondence between computations in Nabla and the search for proofs in a suitable fragment of first order linear logic. Moreover, the translation is not an encoding, meaning that to the algebraic structure of Nabla programs is assigned logical meaning through a non-trivial use of linear logic connectives, as opposed to merely reflecting their operational behavior through a simulation into terms of the logic. In this way we hope that the connection established between the two formalisms can compe...