Last episode discussing Observational Equality Now for Good

Published: April 13, 2023, 5 a.m.

b'

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!".\\xa0 I talk a bit about the structure of the normalization proof in the paper, which uses induction recursion.\\xa0 See this paper by Peter Dybjer for more about that feature.\\xa0 Also, feel free to join the new Telegram group for the podcast if you want to discuss episodes.

'