From the π-calculus to Flat GHC

摘要

We formalize a translation of an asynchronous π-calculus into Flat GHC which does not disrupt too much the intuitive correspondence between them, specially in which regards names vs. logical variables. However, our approach depends on the introduction of some artifacts, namely channel managers. Contrasting other studies, here the communication between managers and other processes is asynchronous. Although this approach is justified by a relaxed notion of compositionality for process algebras, we still need some methodology that allows us to reason about programs in the presence of managers. We show how techniques from program transformation and a form of dynamic search strategy can cope with this. The encoding has been implemented in Haskell and executable programs are obtained from asynchronous π-calculus specifications by means of the KLIC compiler. Alternatively, we have developed in Prolog an interpreter for Flat GHC that has proven useful to analyze aspects of the translation.