Subtyping dependent types

被引：28

作者：

Aspinall, D

Compagnoni, A

机构：

[1] Univ Edinburgh, Div Informat, LFCS, Edinburgh EH9 3JZ, Midlothian, Scotland

[2] Stevens Inst Technol, Dept Comp Sci, Hoboken, NJ 07030 USA

来源：

THEORETICAL COMPUTER SCIENCE | 2001年 / 266卷 / 1-2期

基金：

英国工程与自然科学研究理事会;

关键词：

type theory; dependent types; subtyping;

D O I：

10.1016/S0304-3975(00)00175-4

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

The need for subtyping in type systems with dependent types has been realized for some years. But it is hard to prove that systems combining the two features have fundamental properties such as subject reduction. Here we investigate a subtyping extension of the system lambdaP, which is an abstract version of the type system of the Edinburgh Logical Framework LF. By using an equivalent formulation, we establish some important properties of the new system lambdaP(less than or equal to), including subject reduction. Our analysis culminates in a complete and terminating algorithm which establishes the decidability of type-checking. (C) 2001 Published by Elsevier Science B.V.

引用

页码：273 / 309

页数：37

共 27 条

[1] Subtyping dependent types [J].

Aspinall, D ;

Compagnoni, A .

11TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1996, :86-97

[2]

ASPINALL D, 1977, THESIS U EDINBURGH

[3]

ASPINALL D, 1995, LECT NOTES COMPUTER, V933

[4]

Avron A., 1992, Journal of Automated Reasoning, V9, P309, DOI 10.1007/BF00245294

[5]

Barendregt Henk P., 1992, HDB LOGIC COMPUTER S

[6]

BETARTE G, 1997, P 25 YEARS CONSTR TY

[7] INHERITANCE AS IMPLICIT COERCION [J].

BREAZUTANNEN, V ;

COQUAND, T ;

GUNTER, CA ;

SCEDROV, A .

INFORMATION AND COMPUTATION, 1991, 93 (01) :172-221

[8]

CARDELLI L, 1988, 15 P ACM S PRINC PRO, P70

[9]

CARDELLI L, 1987, LECT NOTES COMPUTER, V306

[10]

CHEN G, 1997, LECT NOTES COMPUTER, V1295, P189

← 1 2 3 →