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'll start out using this blog as a progress tracker, and maybe eventually I'll have the go to write some exposition that may be helpful to others. For now, expect self-indulgent omission of details! By way of introduction, though, I ought to explain some of what I'm currently doing so that future updates will have some context. My primary research project is formalizing the metatheory of LF in Twelf  (colloquially, "LFinLF," because LF is the underlying representation theory of Twelf).  What I am ultimately proving is decidability of typechecking for a dependent type theory; how  I am proving it is syntactically, without logical relations, via translation to syntactic canonical forms.  Chantal Keller presented  essentially the simply-typed case of what I am doing during one of the ICFP workshops this past fall, with two significant departures: for one, her canonical forms presentation was given in spine form (a more focussing-inspired syntactic separation w...