Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/1977| Título: | Type-based termination of recursive definitions |
| Autor(es): | Barthe, Gilles Jacques Denis Frade, M. J. Giménez, E. Pinto, Luís F. Uustalu, Tarmo |
| Palavras-chave: | Type theory Lambda-calculus Termination |
| Data: | 2004 |
| Editora: | Cambridge University Press |
| Revista: | Mathematical Structures in Computer Science |
| Citação: | "Mathematical structures in computer science". ISSN 0960-1295. 14:1 (2004) 97-141. |
| Resumo(s): | This paper introduces "lambda-hat", a simply typed lambda calculus supporting inductive types and recursive function definitions with termination ensured by types. The system is shown to enjoy subject reduction, strong normalisation of typable terms and to be stronger than a related system "lambda-G" in which termination is ensured by a syntactic guard condition. The system can, at will, be extended to also support coinductive types and corecursive function definitions. |
| Tipo: | Artigo |
| URI: | https://hdl.handle.net/1822/1977 |
| DOI: | 10.1017/S0960129503004122 |
| ISSN: | 0960-1295 1469-8072 |
| Arbitragem científica: | yes |
| Acesso: | Acesso aberto |
| Aparece nas coleções: | DI/CCTC - Artigos (papers) |
Ficheiros deste registo:
| Ficheiro | Descrição | Tamanho | Formato | |
|---|---|---|---|---|
| TBterm.pdf | 441,01 kB | Adobe PDF | Ver/Abrir |
