And one more update due to a paper I wrote for the Models of Computation course. I'd like to attend you all to a very beautiful model of computation called interaction nets. One application this model is used for is to optimally implement lambda calculus in a certain theoretical sense.
The paper I wrote connects the Post correspondence problem (PCP) to interaction nets, by reducing PCP in a number of steps to an interaction net and giving some suggestions for the other way around. (Thereby proving interaction nets at least Turing complete, and leaving the suggestion for Turing equivalence.)
The reverse proof is much more involved, needing multiple reduction steps, possibly through the chemical abstract machine I referenced.
I hope some of you will be inspired by interaction nets.
You can find the paper here.
A blag containing my current adventures in logic, haskell and agents.