Intro
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 whe