I'm currently reading Types and Programming Languages by Benjamin C. Pierce and just arrived at chapter 21 Metatheory of Recursive Types.

Prior to this chapter I found the book challenging but comprehensible, but I'm lost on this chapter. Almost none of the definition make intuitively sense to me. Are there any more accessible resources regarding the principle of (co-)induction, tree types and least and greatest fixed points as defined in chapter 21?

  • $\begingroup$ I agree the presentation is quite involved. I did my way to coinduction through the theory of coalgebras. However, I'm not aware of better references for this setting $\endgroup$ Dec 28, 2019 at 12:23


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.