多相型付きラムダ計算
polymorphic typed λ-calculus
二階型付きラムダ計算とも言う
System Fとだいたい同じ(?)