Server OK (belated)

I recently finished LFinLF, a mechanized proof of the metatheory of LF, which took me about two and a half years and 36,503 lines of Twelf. I should focus my exposition efforts about it into a paper, but I thought I should update the occasional follower of this blog with the result.

There are a few remaining questions I have been intrigued to consider as a result of finishing this proof:

  • Can the common folklore that "we don't need family-level lambdas" be made formal? I used them in my proof to define translation: all LF terms translate to normal Canonical LF terms by way of eta-expansion; for families to be treated similarly, we need lambdas to expand the ones at pi kind. But there are other ways to do it which I think would shed varying degrees of light on why we do without them.
  • This proof formalizes the correctness of (a particular algorithm for) LF type checking; could we also verify type reconstruction?
  • Could I formalize the (also folkloric, though from slightly different folk) idea that it would be harmless to add a) type operators and b) base type polymorphism to LF?


Popular posts from this blog

Using Twine for Games Research (Part II)

Reading academic papers while having ADHD

Using Twine for Games Research (Part III)