Self-reference
-- recursive types
F_{ %m }
%t ::= ... | %m %a. %t [%a]
e ::= ... | %l( self ).{ a1 = e_1, ..., a_n = e_n }
Type assignment
\ffrac{
%G |- e_i : %t_i
\hspace{1cm}
(i = 1..n)
}{
%G |- %l( self ).{ a1 = %t_1,.., a_n = %t_n } \e %m%a.{ a1:%t_1,.., a_n : %t_n }[%a]
}
Refinement
\ffrac{
%G, %a <= %b |- %s <= %t
}{
%G |- %m %a.%s[%a] <= %m %b.%t [%b]
}
slide
:
A calculus for recursive types
