Lambda the Ultimate

I just happened to notice that the 13th International SPIN Workshop is coming up. While model checking is kind of off topic, it made me think about SPIN's model checking language Promela.

From the Promela Reference manual:

The language allows for the dynamic creation of concurrent processes. Communication via message channels can be defined to be synchronous (i.e., rendez-vous), or asynchronous (i.e., buffered)

Gerard J. Holzmann's excellent book: The SPIN Model Checker has a complete reference to this interesting C-like language with CSP influenced extensions.