The Locally Nameless Representation

Iowa Type Theory Commute by Aaron Stump

I discuss what is called the locally nameless representation of syntax with binders, following the first couple of sections of the very nicely written paper "The Locally Nameless Representation," by Charguéraud. I compla...View more