[mafribe]

Two brief comments:

(1) The λ-calculus is better thought of as the MVP of SEQUENTIAL programming languages. It is not a good formalism for concurrency. Thee π-calculus is more suitable for concurrency, and, in a real sense, subsumes λ-calculus (see R. Milner's "Functions as Processes" and its subsequent elaborations for details).

(2) Proofs = λ-terms works best for CONSTRUCTIVE logic. With classical logic where not-not-A = A, it kind of works, but not really well.

[DanWaterworth]

(1) I don't think that's fair to say. The lambda calculus is a way of expressing computations with little regard for how they are actually executed.

(2) True, it works better if you add continuations.

[chrismonsanto]

re 1) one of the primary limitations of the lambda calculus wrt concurrency is that it does not model time--there is no way to determine how long a computation takes. An example of a function the lambda calculus cannot define is f(x, y) where the fastest computation of x and y wins. You'll see that function pop up in a number of places in the Haskell world, where it is called "amb". This function is obviously important from a pragmatic POV but it turns out it is also important when doing formal work as well: see the parallel-or/full abstraction problem for PCF[0].

My personal favorite concurrency formalism is the Chemical Abstract Machine[1]. The y-calculus is a neat extension that preserves the spirit of the lambda calculus, but also permits (purely non-deterministic) concurrency.

[0]: http://en.wikipedia.org/wiki/Fully_abstract#Abstraction

[1]: http://www.lix.polytechnique.fr/~fvalenci/papers/cham.pdf

[mafribe]

Most process calculi (including the CHAM) don't model time. I think it's perfectly possible to consider computation without timing.

Adding timing is straightforward for any model of computation with operational semantics. This addition generally changes the semantics dramatically (eg. equalities that hold). There are many timed versions of process calculus, e.g. timed CCS, timed CSP, timed pi-calculus.

[mafribe]

As to (1) I disagree, it's difficult to express general concurrent/parallel computation in lambda-calculus. You need to resort to encodings. That's why process calculi were invented.

Regarding (2), I'm afraid I also disagree. While continuations can express classical logic in some way, it's generally only possible to express certain cut elimination strategies (e.g. call-by-value, as in the Stewart-Ong lambda-mu-calculus). I don't think we know how to do all of classical logic yet. Moreover, adding jumps (which is what continuations are) to lambda-calculus results in an extremely complicated and hard to understand system (e.g. the reduction semantics of the lambda-mu-calculus is usually only handwaved). If you write the very same semantics in pi-calculus, it's trivial and extremely transparent (see "Control in the Pi-Calculus" by Honda et al). Finally, I think it's conceptually deeply confused to 'add' continuations to lambda-calculus. A much cleaner picture emerges when one understands that the call-return jumping discipline engendered by the function-calls of lambda-calculus is a special case of the general jumping that continuations can do. So really one should start with a continuation calculus, and can then see lambda-calculus as a strict sub-calculus of especially disciplined jumps (call-return with affine usage of the return jump).

[DanWaterworth]

w.r.t (1), it's interesting that you and the other replier thought that I meant LC was good for expressing concurrent processes. What I actually meant was that it was also bad at expressing sequential processes, because it doesn't have a single agreed upon operational semantics and it's too high level.