Iowa Type Theory Commute
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
Iowa Type Theory Commute
Last episode discussing Observational Equality Now for Good
•
Aaron Stump
•
Season 4
•
Episode 9
In this episode, I conclude my discussion of some (but hardly all!) points from Pujet and Tabareau's POPL 2022 paper, "Observational Equality -- Now for Good!". I talk a bit about the structure of the normalization proof in the paper, which uses induction recursion. See this paper by Peter Dybjer for more about that feature. Also, feel free to join the new Telegram group for the podcast if you want to discuss episodes.