Much more dramatically, however, the framework can be seen as presenting higher-order (and if desired, constraint-enriched) versions of a variety of other asynchronous concurrent systems, including the asynchronous (``input guarded'') fragment of the (first-order) pi-calculus, Hewitt's actors formalism, (abstract forms of) Gelernter's Linda, asynchronous assignment-based languages, and Petri nets. It can also be seen as smoothly layering around the functional programming style provided by the lambda-calculus a minimal amount of extra logical machinery needed to obtain concurrency, synchronization and indeterminism declaratively. Additionally, there are remarkably simple and direct translations of the untyped lambda-calculus into the higher-order linear CC (HLCC) programming paradigm.
We give (1) a simple operational semantics for HLCC, (2) establish several connections between proof-theory and operational semantics, (3) develop the notion of bi- and equi-simulation for HLCC, along the lines of [CHOCS], (4) establish that logical equivalence implies equi-similarity, (5) show how to obtain the effect of recursion for parametrized processes, (6) demonstrate embeddings of the (asynchronous) pi-calculus and untyped lambda-calculus into HLCC.
In summary, this paper draws on ideas from logic and proof theory to present a framework for the design and analysis of concurrent programming languages.