计算机应用与软件2024，Vol.41Issue(12)：1-8,8.DOI:10.3969/j.issn.1000-386x.2024.12.001
多态性λ-演算的直观建模
INTUITIVE MODELING OF POLYMORPHIC λ-CALCULUS
摘要
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<:)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.关键词
多态性λ-演算/命名绑定/图形重写/建模Key words
Polymorphic λ-calculus/Name binding/Graph rewriting/Modeling分类
信息技术与安全科学引用本文复制引用
阿力木江·亚森,阿布都克力木·阿布力孜,沙尔旦尔·帕尔哈提,哈里旦木·阿布都克里木,朱义鑫..多态性λ-演算的直观建模[J].计算机应用与软件,2024,41(12):1-8,8.基金项目
2018年新疆维吾尔自治区高层次人才引进项目(40050027) （40050027）
2018年新疆维吾尔自治区科学技术厅天池博士项目(40050033) （40050033）
国家自然科学基金项目(61866035,61966033) （61866035,61966033）
新疆维吾尔自治区自然科学基金项目(2020D01A35) （2020D01A35）
四川省科技计划重大科技专项(2020YFQ0018). （2020YFQ0018）
