Constructor subtyping

doi:10.1007/3-540-49099-X_8

Utilize este identificador para referenciar este registo: https://hdl.handle.net/1822/2038

Título:	Constructor subtyping
Autor(es):	Barthe, Gilles Jacques Denis Frade, M. J.
Palavras-chave:	Type theory Lambda-calculus Subtyping
Data:	1999
Editora:	Springer
Revista:	Lecture Notes in Computer Science
Citação:	SWIERSTRA, S. Doaites, ed. lit. – “Programming languages and systems : 8th European Symposium on Programming, ESOP '99, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS '99, Amsterdam, The Netherlands, March 22-28, 1999 : proceedings”. Berlin [etc.] : Springer, 1999. ISBN 3-540-65699-5. p.
Resumo(s):	Constructor subtyping is a form of subtyping in which an inductive type A is viewed as a subtype of another inductive type B if B has more constructors than A. Its (potential) uses include proof assistants and functional programming languages. In this paper, we introduce and study the properties of a simply typed lambda-calculus with record types and datatypes, and which supports record subtyping and constructor subtyping. In the first part of the paper, we show that the calculus is confluent and strongly normalizing. In the second part of the paper, we show that the calculus admits a well-behaved theory of canonical inhabitants, provided one adopts expansive extensionality rules, including eta-expansion, surjective pairing, and a suitable expansion rule for datatypes. Finally, in the third part of the paper, we extend our calculus with unbounded recursion and show that confluence is preserved.
Tipo:	Artigo em ata de conferência
URI:	https://hdl.handle.net/1822/2038
ISBN:	3-540-65699-5
DOI:	10.1007/3-540-49099-X_8
ISSN:	0302-9743
Arbitragem científica:	yes
Acesso:	Acesso aberto
Aparece nas coleções:	HASLab - Artigos em revistas internacionais DI/CCTC - Artigos (papers)