Inserting declaration into Gamma ================================ For each method def m[A](x_1:T_1, ..., x_n:T_n) : T = { ... } we insert into Gamma the pair: (m,\forall A. T_1 x ... T_n -> T) Method call rule for a single type parameter ============================================ (m,\forall A. T_1 x ... T_n -> T) in Gamma Gamma |- e_i : S_i S_i = T_i[A:=T0] S = T[A:=T0] ------------------------------------------- Gamma |- m[T0](e_1,...,e_n) : S Type checking method body ========================= For method def m[A](x_1:T_1, ..., x_n:T_n) : T = e we check that Gamma + { (x_1,T_1),...,(x_n,T_n)} |- e : T In other words, the type checking rule remains the same as without generic types, but now the type variables such as A may occur as types in the environment.