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?


Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.