Subtyping dependent types (Summary)

David Aspinall; Adriana Compagnoni

doi:10.1109/LICS.1996.561307

Subtyping dependent types (Summary)

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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 λP, 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 λP⩽, including subject reduction. Our analysis culminates in a complete and terminating algorithm which establishes the decidability of type-checking

Original language	English
Title of host publication	LICS '96. Proceedings., Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996
Publisher	Institute of Electrical and Electronics Engineers
Pages	86-97
Number of pages	10
ISBN (Print)	0-8186-7463-6
DOIs	https://doi.org/10.1109/LICS.1996.561307
Publication status	Published - 1996

Access to Document

10.1109/LICS.1996.561307

http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=561307&punumber%3D4265%26sortType%3Dasc_p_Sequence%26filter%3DAND%28p_IS_Number%3A12231%29%26pageNumber%3D2

Cite this

@inproceedings{799100cd62bc4492a88b10b263f57cac,

title = "Subtyping dependent types (Summary)",

abstract = "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 λP, 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 λP⩽, including subject reduction. Our analysis culminates in a complete and terminating algorithm which establishes the decidability of type-checking",

author = "David Aspinall and Adriana Compagnoni",

year = "1996",

doi = "10.1109/LICS.1996.561307",

language = "English",

isbn = "0-8186-7463-6",

pages = "86--97",

booktitle = "LICS '96. Proceedings., Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996",

publisher = "Institute of Electrical and Electronics Engineers",

address = "United States",

}

TY - GEN

T1 - Subtyping dependent types (Summary)

AU - Aspinall, David

AU - Compagnoni, Adriana

PY - 1996

Y1 - 1996

N2 - 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 λP, 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 λP⩽, including subject reduction. Our analysis culminates in a complete and terminating algorithm which establishes the decidability of type-checking

AB - 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 λP, 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 λP⩽, including subject reduction. Our analysis culminates in a complete and terminating algorithm which establishes the decidability of type-checking

U2 - 10.1109/LICS.1996.561307

DO - 10.1109/LICS.1996.561307

M3 - Conference contribution

SN - 0-8186-7463-6

SP - 86

EP - 97

BT - LICS '96. Proceedings., Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996

PB - Institute of Electrical and Electronics Engineers

ER -

Subtyping dependent types (Summary)

Abstract

Access to Document

Fingerprint

Cite this