Existential types -- hiding

F_{ \E }


Type assignment

Refinement

  • \ffrac{ %G |- %s <= %s' \hspace{1cm} %G |- %t' <= %t }{ %G |- \E %a <= %s' . %t' <= \E %a <= %s. %t }

slide: The existential type calculus