Intersection types -- overloading

%l_{ /\ }


Type assignment

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