Linearity and iterator types for Gödel's System ¿

• Tipo: Artigo em Revista Científica Internacional
• Data: 2010

Autores

Alves, S (Autor) FCUP; Fernandez, M (Autor) Outra; Florido, M (Autor) FCUP; MacKie, I (Autor) Outra

Revista

Título: Higher-Order and Symbolic Computation

Vol. 23 Nº 1

Páginas: 1-27

ISSN: 1388-3690

Editora: Kluwer Academic Publishers

Indexação

ISI Web of Knowledge

Scopus - 2 Citações

Outras Informações

ID Authenticus: P-007-ZRB

DOI: 10.1007/s10990-010-9060-x

Abstract (EN): System ¿ ¿ is a linear ¿-calculus with numbers and an iterator, which, although imposing linearity restrictions on terms, has all the computational power of Gödel's System ¿. System ¿¿ owes its power to two features: the use of a closed reduction strategy (which permits the construction of an iterator on an open function, but only iterates the function after it becomes closed), and the use of a liberal typing rule for iterators based on iterative types. In this paper, we study these new types, and show how they relate to intersection types. We also give a sound and complete type reconstruction algorithm for System ¿¿. © 2010 Springer Science+Business Media, LLC.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 27