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 MackieSystem 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 ComputationISSN
13883690Publisher
SpringerExternal DOI
Issue
1Volume
23Page range
1-27Department affiliated with
- Informatics Publications
Full text available
- No
Peer reviewed?
- Yes
Legacy Posted Date
2012-02-06Usage metrics
Categories
No categories selectedKeywords
Licence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC