Iowa Type Theory Commute

The Locally Nameless Representation


Listen Later

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.  

View all episodesView all episodes
Download on the App Store

Iowa Type Theory CommuteBy Aaron Stump

  • 5
  • 5
  • 5
  • 5
  • 5

5

16 ratings