Alves, Sandra, Fernández, Maribel, Florido, Mário and Mackie, Ian (2010) Linearity and Iterator Types for Godel's System T. Higher-Order and Symbolic Computation, 23 (1). pp. 1-27. ISSN 13883690
Full text not available from this repository.Abstract
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 .
Item Type: | Article |
---|---|
Schools and Departments: | School of Engineering and Informatics > Informatics |
Depositing User: | Ian Mackie |
Date Deposited: | 06 Feb 2012 19:54 |
Last Modified: | 07 Jun 2012 13:40 |
URI: | http://sro.sussex.ac.uk/id/eprint/22858 |