Holodeck games and CCCs

From the n-Category Cafe, some notes on Holodeck Games and cartesian closed categories.

This also appeared here (and was mentioned by Phil Wadler). The two posts seem to have different addenda, comments and links, so it may be worth looking at both.

It's fun to see lambda calculus introduced to an audience already familiar with categories, as that seems to be the opposite of the usual state of affairs around here, and I can think of certain LtU regulars who will hopefully find this whole subject enjoyable.