University of Sussex
Browse

File(s) not publicly available

Linearity and Iterator Types for Godel's System T

journal contribution
posted on 2023-06-08, 00:28 authored by Sandra Alves, Maribel Fernández, Mário Florido, Ian MackieIan Mackie
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 .

History

Publication status

  • Published

Journal

Higher-Order and Symbolic Computation

ISSN

13883690

Publisher

Springer

Issue

1

Volume

23

Page range

1-27

Department affiliated with

  • Informatics Publications

Full text available

  • No

Peer reviewed?

  • Yes

Legacy Posted Date

2012-02-06

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC