多态性λ-演算的直观建模OA北大核心CSTPCD

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<:)by using a modeling language called HyperLMNtal.The models were tested by benchmarks from the PoplMark challenge.Experimental results show that this technique is suitable for rapid modeling of complex formal systems,because it enables programmers to turn theory into practice without re-formalization.