I don't fully agree with Pfenning here. The pi-calculus is not that good a proof system for linear logic: pi-calculus imposes sequentiality constraints on proofs that impede parallelism. Take for example the term

     x!<a> | y!<b> | x?(c).y?(d).P

You have to sequentialise the two possible reductions on x and y. The culprit is the pi-calculus's input prefix, which combines two operations: blocking input and scoping of the bound variables (here c and d). This sequentialisation is not true to the spirit of linear logic proofs (think e.g. proof nets).

Conversely, I don't think linear logic is a good typing system for pi-calculus for a variety of reasons: among them that linear logic does not track causality well, and because it doesn't take care of affine (at most once) interactions well.

These are good points and I'll have to consider them. I was planning on going back through Pfenning's notes again in a bit and I'll keep a more critical eye this next time. Thanks!

(Also, to be clear and with reference to other threads we've conversed on here, I think of linear logic and pi calculus, even if they aren't well-corresponding, as fantastic, unavoidable examples of non-function-application style programming.)