University of Udine University of Udine

The POPLmark Challenge: subtyping


Alberto Ciaffaglione, Ivan Scagnetto

The inductive definition of algorithmic subtyping: 

                                                X<:U in Gamma   Gamma |- U<:T
---------------          -------------          -----------------------------
Gamma |- S<:Top          Gamma |- X<:X                  Gamma |- X<:T

Gamma |- T1<:S1   Gamma |- S2<:T2     Gamma |- T1<:S1   Gamma,X<:T1 |- S2<:T2
--------------------------------   ------------------------------------------
    Gamma |- S1->S2 <: T1->T2       Gamma |- forall X<:S1.S2 <: forall X<:T1.T2

Back to the main page