Structural rules, or the Curse of the Bound Variable
Iowa Type Theory Commute
English - October 13, 2021 04:00 - 12 minutes - 8.9 MB - ★★★★★ - 13 ratingsTechnology Science Mathematics programming languages computational logic type theory proof assistants cedille Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
Previous Episode: Why Cut Elimination is More Complicated than Normalization
Next Episode: A taste of linear logic
In this episode I discuss the basic structural rules of weakening, contraction, and exchange, and speculate on their dark origin.