HIGHER-ORDER SUBTYPING

被引：0

作者：

STEFFEN, M ^{[1
]}

PIERCE, B ^{[1
]}

机构：

[1] UNIV EDINBURGH, DEPT COMP SCI, EDINBURGH EH9 3JZ, MIDLOTHIAN, SCOTLAND

来源：

PROGRAMMING CONCEPTS, METHODS AND CALCULI | 1994年 / 56卷

关键词：

OBJECT-ORIENTED PROGRAMMING (D.1.5); FORMAL DEFINITIONS AND THEORY (D.3.1); SEMANTICS OF PROGRAMMING LANGUAGES (F.3.2); STATIC TYPE SYSTEMS; LAMBDA-CALCULUS; POLYMORPHISM; SUBTYPING;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

System F-less than or equal to(w) is an extension with subtyping of Girard's higher-order polymorphic lambda-calculus. We develop the fundamental metatheory of this calculus: decidability of beta-conversion on well-kinded types, elimination of the ''cut-rule'' of transitivity from the subtype relation, and the soundness, completeness, and termination of algorithms for subtyping and typechecking.

引用

页码：511 / 530

页数：20

共 50 条

[1] Higher-order subtyping
Pierce, B
Steffen, M
[J]. THEORETICAL COMPUTER SCIENCE, 1997, 176 (1-2) : 235 - 282
[2] Higher-order subtyping and its decidability
Compagnoni, A
[J]. INFORMATION AND COMPUTATION, 2004, 191 (01) : 41 - 103
[3] Syntactic Metatheory of Higher-Order Subtyping
Abel, Andreas
Rodriguez, Dulma
[J]. COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2008, 5213 : 446 - 460
[4] Foundations for the implementation of higher-order subtyping
Crary, K
[J]. ACM SIGPLAN NOTICES, 1997, 32 (08) : 125 - 135
[5] Anti-symmetry of higher-order subtyping and equality by subtyping
Compagnoni, A
Goguen, H
[J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2006, 16 (01) : 41 - 65
[6] A typed semantics of higher-order store and subtyping
Schwinghammer, J
[J]. THEORETICAL COMPUTER SCIENCE, PROCEEDINGS, 2005, 3701 : 390 - 405
[7] Decidability of higher-order subtyping with intersection types
Compagnoni, AB
[J]. COMPUTER SCIENCE LOGIC, 1995, 933 : 46 - 60
[8] Typed operational semantics for higher-order subtyping
Compagnoni, A
Goguen, H
[J]. INFORMATION AND COMPUTATION, 2003, 184 (02) : 242 - 297
[9] A Theory of Higher-Order Subtyping with Type Intervals
Stucki, Sandro
Giarrusso, Paolo G.
[J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2021, 5
[10] Anti-symmetry of higher-order subtyping
Compagnoni, A
Goguen, H
[J]. COMPUTER SCIENCE LOGIC, PROCEEDINGS, 1999, 1683 : 420 - 438

← 1 2 3 4 5 →