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

• Type: Article in International Scientific Journal
• Date: 2010

Authors

Alves, S (Author) FCUP; Fernandez, M (Author) Other; Florido, M (Author) FCUP; MacKie, I (Author) Other

Journal

Title: Higher-Order and Symbolic Computation

Vol. 23 No. 1

Pages: 1-27

ISSN: 1388-3690

Publisher: Kluwer Academic Publishers

Indexing

ISI Web of Knowledge

Scopus - 2 Citations

Other information

Authenticus ID: 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.

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 27