A simple type calculus
-- subtypes
%l_{ <= }
%t ::= %r | %t_1 -> %t_2
e ::= x | %l x : %t . e | e_1 e_2
Type assignment
\ffrac{
%G |- x : %s
\hspace{1cm}
%G |- e : %t
}{
%G |- %l x : %s . e \e %s -> %t
}
\ffrac{
%G |- e_1 : %s -> %t, e_2 : %s
}{
%G |- e_1 e_2 \e %t
}
Refinement
\ffrac{
%G |- e : %s
\hspace{1cm}
%G |- %s <= %t
}{
%G |- e : %t
}
slide
:
The subtype calculus
