*logic*programming language --- I can't really account for the peculiar symmetric negotiation between reads and writes that the synchronous pi calculus does (if I remember right) but execution of process P in the asynchronous pi calculus seems to be utterly explainable-away as focusing proof search for a proof of P* |- 1, given the translation

(P + P)* = (P* & P*) 0* = 1 (P | P)* = P* tensor P* (nu x.P)* = exists x . P* (!P)* = !(P*) (c(x).P)* = all x . msg(c,x) -o P* (c<d>)* = msg(c,d)

where the quantifiers range over some first-order domain of "channels", and msg is some positive atom that takes two channels.