We propose a simple untyped calculus inspired by the proofs encoding of Linear Logic by Girard. The basic elements of our calculus are multisets of terms sharing a workspace and they dynamic behaviour is defined by a reduction semantics in the style of the Chemical Abstract Machine. We address the issue of treating concurrency via a model of computation whose basic step can be interpreted as cut elimination. The expressive power of our calculus is shown by providing encodings for the lambda calculus and the fusion calculus.
Functional Features of a Calculus for Logic and Concurrency
SOLITRO, Ugo
2000-01-01
Abstract
We propose a simple untyped calculus inspired by the proofs encoding of Linear Logic by Girard. The basic elements of our calculus are multisets of terms sharing a workspace and they dynamic behaviour is defined by a reduction semantics in the style of the Chemical Abstract Machine. We address the issue of treating concurrency via a model of computation whose basic step can be interpreted as cut elimination. The expressive power of our calculus is shown by providing encodings for the lambda calculus and the fusion calculus.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
