Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/2044
Título: | Constructor subtyping: extended version |
Autor(es): | Frade, M. J. Barthe, Gilles Jacques Denis |
Palavras-chave: | Type theory Lambda-calculus Inductive types Subtyping Overloading |
Data: | Jun-1999 |
Editora: | Universidade do Minho. Departamento de Informática |
Citação: | BARTHE, Gilles ; FRADE, Maria João – “Constructor subtyping : extended version” [Em linha]. [S.l.] : Universidade do Minho. Departamento de Informática, 1999. [Consult. 8 Jun. 2005]. Disponível em: http://www.di.uminho.pt/~mjf/publications |
Resumo(s): | Constructor subtyping is a form of subtyping in which an inductive type $\sigma$ is viewed as a subtype of another inductive type $\tau$ if $\tau$ has more elements than $\sigma$. Its (potential) uses include proof assistants and functional programming languages. In this report, we introduce and study the properties of a simply typed $\lambda$-calculus which supports constructor subtyping. We show that the calculus is well-behaved and provides a suitable basis for formalizing natural semantics in proof-development systems. |
Tipo: | Relatório |
URI: | https://hdl.handle.net/1822/2044 |
Acesso: | Acesso aberto |
Aparece nas coleções: | DI/CCTC - Relatórios Técnicos |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
CSrep-Feb99.ps | 839,34 kB | Postscript | Ver/Abrir | |
CSrep-Feb99.pdf | 713,76 kB | Adobe PDF | Ver/Abrir |