Iterator Types

Abstract. System L is a linear λ-calculus with numbers and an iterator, which, although imposing linearity restrictions on terms, has all the computational power of G¨odel’s System T . System L 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 L.

• Type: Conference
• Year: 2007
• Where: FOSSACS
• Authors: Sandra Alves, Maribel Fernández, Mário Florido, Ian Mackie
• Keywords: Applied Computing, Closed Reduction Strategy, FOSSACS 2007, Liberal Typing Rule, Linearity Restrictions