Intersection types
-- overloading
%l_{ /\ }
%t ::= %r | %t_1 -> %t_2 | \bigwedge [ %t_1 .. %t_n ]
Type assignment
\ffrac{
%G |- e : %t_i
(i \e 1..n)
}{
%G |- e : \bigwedge [ %t_1 .. %t_n ]
}
Refinement
\ffrac{
%G |- %s <= %t_i
(i \e 1..n )
}{
%G |- %s <= \bigwedge [ %t_1 .. %t_n ]
}
\bigwedge [ %t_1 .. %t_n ] <= %t_i
%G |- \bigwedge [ %s -> %t_1 .. %s -> %t_n ] <= %s -> \bigwedge [ %t_1 .. %t_n ]
slide
:
The intersection type calculus
