The Locally Nameless Representation
Update: 2025-01-03
Description
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 complain due to the statement in the paper that "the theory of λ-calculus identifies terms that are α-equivalent," which is simply not true if one is considering lambda calculus as defined by Church, where renaming is an explicit reduction step, on a par with beta-reduction. I also answer a listener's question about what "computational type theory" means.
Feel free to email me any time at aaron.stump@bc.edu, or join the Telegram group for the podcast.
Comments
In Channel
Download from Google Play
Download from App Store
United States00:00
00:00
x
