Applicative communicating processes in first order logic

We describe a first order applicative language for the specification of deterministic systems of communicating computing agents à la Kahn-MacQueen. Both the sequential and parallel interpreter we give are based on lazy evaluation, are demand driven and can handle infinite streams and non-terminating procedures. An equivalent least fixed-point semantics is then presented which neatly copes with the above features of the language. It is worth nothing that computations in our logic based model can be considered as formal proofs, thus making formal reasoning about programs easier.