(define-language Lambda (e ::= x (lambda (x_!_ ...) e) (e e ...) n (+ e e) (if0 e e e) (spawn e) (put c e) (get c) (void)) (n ::= number) (c ::= variable-not-otherwise-mentioned) (x ::= variable-not-otherwise-mentioned))
Hints Instead of a single expression, your reductions must deal with a set of expressions, one per thread. Reducing (spawn e) in one of these expressions thus adds an e to that set; use (void) as the result of this action. When any one thread has (get c) as its redex and another has (put c v), the two redexes are simultaneously replaced with their contractions.
In Redex, sets are currently realized with sequences. The key difference is that sets are unordered and sequences are ordered. Keep this in mind when you formulate reduction relations for put-get communications.