Everything in Context

I've been distracting myself recently by doing some untyped-lambda-calculus hackery, so I may as well write it up, because I don't think I've seen this particular kind of hackery described elsewhere, and I'm trying to get better at day-to-day documentation. It's kind of cute and probably not very profound, but if anyone sees connections to other work, please point it out. The context is here is that I was attempting to understand Bohm's Theorem (a la [1] or [2]), and Twelf is my usual tool for understanding things about lambda calculi. So I started with the bog-standard Twelf encoding of untyped lambda calculus: exp : type. lam : (exp -> exp) -> exp. app : exp -> exp -> exp. ...with the goal in mind of eventually formalizing Bohm's Theorem. (I do still have that goal in mind, by the way, and will hopefully post about it when completed.) The puzzle is how to write programs over such terms that implement the various meta-level functions

I've been wanting to respond to this essay lamenting the disconnect between PL popularity and PL research  since it started making the rounds earlier this week, and I've wanted to write a post about what I think PL theory and interaction design have to do with one another for even longer ; possibly I can tie these thoughts together in a single post. [WARNING: much fuzzy speculation that lack concrete substantiation herein, but I wanted to put these thoughts together before they dissolve into my subconsciousness any further...] "Programming languages as if people matter" The larger context for these thoughts is the ongoing battle I have been mentally cataloging for years (and which certainly predates my involvement in academic research, so I'm bound to say some misinformed things -- please correct me!), the frequent and frustrating friction between researchers in type theory and logic (in my terms "PL theory") and those who criticize such work for foc