Abstract: Name binding is one of the core concepts in formal systems. As for simplicity and intuitiveness, existing name binding techniques have their advantages and disadvantages. In this paper, a name binding technique based on hypergraph rewriting is applied to the modeling of the type checking and callbyvalue reduction of polymorphic λcalculus with subtypes and records (or System FKG-*4