Self-reference -- recursive types

F_{ %m }


Type assignment

Refinement

  • \ffrac{ %G, %a <= %b |- %s <= %t }{ %G |- %m %a.%s[%a] <= %m %b.%t [%b] }

slide: A calculus for recursive types