### 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:

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?

## Comments

## Post a Comment