In the "hey, wtf didn't you cite this" section of the reviews of my rejected paper are a couple of neat other papers: The Implicit Calculus of Constructions and More on Implicit Syntax . Ambifortunately , these are both about systems with which I am not very familiar at all. An excuse to learn about them, I suppose!