The Locally Nameless Representation

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.

You can listen to The Locally Nameless Representation online on Radio and Podcast. Open the player on this page to stream the available audio.

The Locally Nameless Representation is an episode from Iowa Type Theory Commute by Aaron Stump.

This episode is 19:54 long.

This episode was published on Jan 3, 2025.

Yes. Use the heart button on the episode page to add it to your favorite episodes list.

Yes. This page shows related episodes from Iowa Type Theory Commute when more episodes are available from the podcast feed.