{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:26:53Z","timestamp":1686083213263},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,3,1]],"date-time":"2010-03-01T00:00:00Z","timestamp":1267401600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order Symb Comput"],"published-print":{"date-parts":[[2010,3]]},"DOI":"10.1007\/s10990-010-9060-x","type":"journal-article","created":{"date-parts":[[2010,8,19]],"date-time":"2010-08-19T07:48:08Z","timestamp":1282204088000},"page":"1-27","source":"Crossref","is-referenced-by-count":1,"title":["Linearity and iterator types for G\u00f6del\u2019s System"],"prefix":"10.1007","volume":"23","author":[{"given":"Sandra","family":"Alves","sequence":"first","affiliation":[]},{"given":"Maribel","family":"Fern\u00e1ndez","sequence":"additional","affiliation":[]},{"given":"M\u00e1rio","family":"Florido","sequence":"additional","affiliation":[]},{"given":"Ian","family":"Mackie","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,8,20]]},"reference":[{"key":"9060_CR1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(93)90181-R","volume":"111","author":"S. Abramsky","year":"1993","unstructured":"Abramsky, S.: Computational interpretations of linear logic. Theor. Comput. Sci. 111, 3\u201357 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"9060_CR2","unstructured":"Alves, S.: Linearisation of the lambda calculus. Ph.D. thesis, Faculty of Science, University of Porto (April 2007). Available from http:\/\/www.dcc.fc.up.pt\/sandra\/papers\/PhDthesis.pdf.gz"},{"key":"9060_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/11874683_8","volume-title":"Proceedings of the 15th EACSL Conference on Computer Science Logic (CSL\u201906)","author":"S. Alves","year":"2006","unstructured":"Alves, S., Fern\u00e1ndez, M., Florido, M., Mackie, I.: The power of linear functions. In: \u00c9sik, Z. (ed.) Proceedings of the 15th EACSL Conference on Computer Science Logic (CSL\u201906). Lecture Notes in Computer Science, vol. 4207, pp. 119\u2013134. Springer, Berlin (2006)"},{"key":"9060_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/978-3-540-71389-0_3","volume-title":"Proceedings FOSSACS","author":"S. Alves","year":"2007","unstructured":"Alves, S., Fern\u00e1ndez, M., Florido, M., Mackie, I.: Iterator types. In: Seidl, H. (ed.) Proceedings FOSSACS. Lecture Notes in Computer Science, vol. 4423, pp. 17\u201331. Springer, Berlin (2007)"},{"issue":"10","key":"9060_CR5","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/j.entcs.2007.02.047","volume":"174","author":"S. Alves","year":"2007","unstructured":"Alves, S., Fern\u00e1ndez, M., Florido, M., Mackie, I.: The power of closed-reduction strategies. Electron. Notes Theor. Comput. Sci. 174(10), 57\u201374 (2007). Proceedings of WRS 2006, 6th International Workshop on Rewriting Strategies, FLOC 2006, Seattle","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"11\u201313","key":"9060_CR6","doi-asserted-by":"crossref","first-page":"1484","DOI":"10.1016\/j.tcs.2009.11.014","volume":"411","author":"S. Alves","year":"2010","unstructured":"Alves, S., Fern\u00e1ndez, M., Florido, M., Mackie, I.: G\u00f6del\u2019s System T revisited. Theor. Comput. Sci. 411(11\u201313), 1484\u20131500 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"9060_CR7","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)"},{"key":"9060_CR8","unstructured":"Bakel, S.: Intersection type disciplines in lambda calculus and applicative term rewriting systems. Ph.D. thesis, Department of Computer Science, University of Nijmegen (1993)"},{"issue":"2","key":"9060_CR9","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1016\/0304-3975(95)00073-6","volume":"151","author":"S. Bakel","year":"1995","unstructured":"Bakel, S.: Intersection type assignment systems. Theor. Comput. Sci. 151(2), 385\u2013435 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"9060_CR10","doi-asserted-by":"crossref","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H.P. Barendregt","year":"1983","unstructured":"Barendregt, H.P., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type-assignment. J. Symb. Log. 48, 931\u2013940 (1983)","journal-title":"J. Symb. Log."},{"issue":"4","key":"9060_CR11","doi-asserted-by":"crossref","first-page":"685","DOI":"10.1305\/ndjfl\/1093883253","volume":"21","author":"M. Coppo","year":"1980","unstructured":"Coppo, M., Dezani-Ciancaglini, M.: An extension of the basic functionality theory for the \u03bb-calculus. Notre Dame J. Form. Log. 21(4), 685\u2013693 (1980)","journal-title":"Notre Dame J. Form. Log."},{"key":"9060_CR12","unstructured":"Damas, L.M.M.: Type assignment in programming languages. Ph.D. thesis. University of Edinburgh (1985)"},{"key":"9060_CR13","doi-asserted-by":"crossref","unstructured":"Damas, L.M.M., Milner, R.: Principal type schemes for functional programs. In: Conference Record of the Ninth Annual ACM Symposium on the Principles of Programming Languages, pp. 207\u2013212 (1982)","DOI":"10.1145\/582153.582176"},{"key":"9060_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/11417170_12","volume-title":"TLCA\u201905","author":"F. Damiani","year":"2005","unstructured":"Damiani, F.: Rank-2 intersection and polymorphic recursion. In: TLCA\u201905. Lecture Notes in Computer Science, vol.\u00a03461, pp. 146\u2013161. Springer, Berlin (2005)"},{"issue":"2","key":"9060_CR15","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1017\/S0960129504004633","volume":"15","author":"M. Fern\u00e1ndez","year":"2005","unstructured":"Fern\u00e1ndez, M., Mackie, I., Sinot, F.-R.: Closed reduction: explicit substitutions without alpha conversion. Math. Struct. Comput. Sci. 15(2), 343\u2013381 (2005)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1","key":"9060_CR16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear Logic. Theor. Comput. Sci. 50(1), 1\u2013102 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"9060_CR17","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1016\/S0049-237X(08)70271-4","volume-title":"Logic Colloquium 88","author":"J.-Y. Girard","year":"1989","unstructured":"Girard, J.-Y.: Geometry of interaction 1: Interpretation of System\u00a0F. In: Ferro, R., Bonotto, C., Valentini,\u00a0S., Zanardo, A. (eds.) Logic Colloquium 88. Studies in Logic and the Foundations of Mathematics, vol.\u00a0127, pp. 221\u2013260. North-Holland, Amsterdam (1989)"},{"key":"9060_CR18","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1090\/conm\/092\/1003197","volume-title":"Categories in Computer Science and Logic: Proc. of the Joint Summer Research Conference","author":"J.-Y. Girard","year":"1989","unstructured":"Girard, J.-Y.: Towards a geometry of interaction. In: Gray, J.W., Scedrov, A. (eds.) Categories in Computer Science and Logic: Proc. of the Joint Summer Research Conference, pp. 69\u2013108. Am. Math. Soc., Providence (1989)"},{"key":"9060_CR19","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Proofs and Types","author":"J.-Y. Girard","year":"1989","unstructured":"Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol.\u00a07. Cambridge University Press, Cambridge (1989)"},{"issue":"1\u20133","key":"9060_CR20","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/j.scico.2004.01.004","volume":"50","author":"C. Haack","year":"2004","unstructured":"Haack, C., Wells, J.B.: Type error slicing in implicitly typed higher-order languages. Sci. Comput. Program. 50(1\u20133), 189\u2013224 (2004)","journal-title":"Sci. Comput. Program."},{"key":"9060_CR21","first-page":"32","volume-title":"LICS","author":"J.S. Hodas","year":"1991","unstructured":"Hodas, J.S., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. In: LICS, pp.\u00a032\u201342. IEEE Comput. Soc., Los Alamitos (1991)"},{"issue":"2","key":"9060_CR22","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1006\/inco.1994.1036","volume":"110","author":"J.S. Hodas","year":"1994","unstructured":"Hodas, J.S., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Inf. Comput. 110(2), 327\u2013365 (1994)","journal-title":"Inf. Comput."},{"key":"9060_CR23","unstructured":"Hudak, P., Peterson, J., Fasel, J.: A gentle introduction to Haskell 98. http:\/\/www.haskell.org\/tutorial\/ (1999)"},{"key":"9060_CR24","unstructured":"Jim, T.: Rank 2 type systems and recursive definitions. Technical report. Massachusetts Institute of Technology (1995)"},{"key":"9060_CR25","volume-title":"Proceedings of the 23rd ACM Symposium on Principles of Programming Languages (POPL\u201996)","author":"T. Jim","year":"1996","unstructured":"Jim, T.: What are principal typings and what are they good for? In: Proceedings of the 23rd ACM Symposium on Principles of Programming Languages (POPL\u201996). ACM, New York (1996)"},{"key":"9060_CR26","first-page":"90","volume-title":"Proceedings of the 1999 International Conference on Functional Programming","author":"A.J. Kfoury","year":"1999","unstructured":"Kfoury, A.J., Mairson, H.G., Turbak, F.A., Wells, J.B.: Relating typability and expressibility in finite-rank intersection type systems. In: Proceedings of the 1999 International Conference on Functional Programming, pp. 90\u2013101. ACM, New York (1999)"},{"key":"9060_CR27","first-page":"95","volume-title":"Proceedings of the 17th ACM Symposium on Principles of Programming Languages (POPL\u201990)","author":"Y. Lafont","year":"1990","unstructured":"Lafont, Y.: Interaction nets. In: Proceedings of the 17th ACM Symposium on Principles of Programming Languages (POPL\u201990), pp. 95\u2013108. ACM, New York (1990)"},{"key":"9060_CR28","first-page":"363","volume-title":"To H.B.\u00a0Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"J. Lambek","year":"1980","unstructured":"Lambek, J.: From lambda calculus to Cartesian closed categories. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B.\u00a0Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 363\u2013402. Academic Press, London (1980)"},{"key":"9060_CR29","series-title":"Cambridge Studies in Advanced Mathematics","volume-title":"Introduction to Higher Order Categorical Logic","author":"J. Lambek","year":"1986","unstructured":"Lambek, J., Scott, P.J.: Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics, vol.\u00a07. Cambridge University Press, Cambridge (1986)"},{"key":"9060_CR30","unstructured":"Mackie, I., Lilac: A functional programming language based on linear logic. Master\u2019s thesis, Department of Computing, Imperial College of Science, Technology and Medicine (September 1991)"},{"issue":"4","key":"9060_CR31","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1017\/S0956796800001131","volume":"4","author":"I. Mackie","year":"1994","unstructured":"Mackie, I.: Lilac: A functional programming language based on linear logic. J. Funct. Program. 4(4), 395\u2013433 (1994)","journal-title":"J. Funct. Program."},{"issue":"3","key":"9060_CR32","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/BF00873993","volume":"1","author":"I. Mackie","year":"1993","unstructured":"Mackie, I., Rom\u00e1n, L., Abramsky, S.: An internal language for autonomous categories. Appl. Categ. Struct. 1(3), 311\u2013343 (1993)","journal-title":"Appl. Categ. Struct."},{"issue":"2","key":"9060_CR33","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Trans. Program. Lang. Syst. 4(2), 258\u2013282 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"9060_CR34","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17(3), 348\u2013375 (1978)","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"9060_CR35","doi-asserted-by":"crossref","first-page":"223","DOI":"10.2307\/1968867","volume":"43","author":"M. Newman","year":"1942","unstructured":"Newman, M.: On theories with a combinatorial definition of \u201cequivalence. Ann. Math. 43(2), 223\u2013243 (1942)","journal-title":"Ann. Math."},{"key":"9060_CR36","first-page":"535","volume-title":"To H.B.\u00a0Curry, Essays in Combinatory Logic, Lambda-Calculus and Formalism","author":"G. Pottinger","year":"1980","unstructured":"Pottinger, G.: A type assignment for strongly normalizable \u03bb-terms. In: To H.B.\u00a0Curry, Essays in Combinatory Logic, Lambda-Calculus and Formalism, pp. 535\u2013560. Academic Press, New York (1980)"},{"issue":"1","key":"9060_CR37","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"9060_CR38","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Proceedings L.E.J.\u00a0Brouwer Centenary Symposium, 1981","author":"H. Schwichtenberg","year":"1982","unstructured":"Schwichtenberg, H.: Complexity of normalization in the pure typed lambda-calculus. In: Proceedings L.E.J.\u00a0Brouwer Centenary Symposium, 1981. Studies in Logic and the Foundations of Mathematics, vol. 110. North-Holland, Amsterdam (1982)"},{"key":"9060_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1007\/3-540-19242-5_17","volume-title":"Proceedings of the 1st International Workshop on Conditional Term Rewriting Systems, CTRS\u201987, Orsay, France","author":"Y. Toyama","year":"1988","unstructured":"Toyama, Y.: Confluent term rewriting systems with membership. In: Proceedings of the 1st International Workshop on Conditional Term Rewriting Systems, CTRS\u201987, Orsay, France. Lecture Notes in Computer Science, vol. 308, pp. 228\u2013241. Springer, Berlin (1988)"},{"key":"9060_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/3-540-56393-8_29","volume-title":"Proceedings of the 3rd International Workshop on Conditional Term Rewriting Systems, CTRS\u201992, Pont-\u00e0-Mousson, France","author":"J. Yamada","year":"1993","unstructured":"Yamada, J.: Confluence of terminating membership conditional TRS. In: Proceedings of the 3rd International Workshop on Conditional Term Rewriting Systems, CTRS\u201992, Pont-\u00e0-Mousson, France. Lecture Notes in Computer Science, vol. 656, pp. 378\u2013392. Springer, Berlin (1993)"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-010-9060-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10990-010-9060-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-010-9060-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,2]],"date-time":"2019-06-02T03:00:54Z","timestamp":1559444454000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10990-010-9060-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,3]]},"references-count":40,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,3]]}},"alternative-id":["9060"],"URL":"https:\/\/doi.org\/10.1007\/s10990-010-9060-x","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,3]]}}}