{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,6]],"date-time":"2026-01-06T17:30:39Z","timestamp":1767720639288,"version":"3.40.3"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319296036"},{"type":"electronic","value":"9783319296043"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-29604-3_6","type":"book-chapter","created":{"date-parts":[[2016,2,20]],"date-time":"2016-02-20T07:53:12Z","timestamp":1455954792000},"page":"80-93","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["An Interaction Net Encoding of G\u00f6del\u2019s System\u00a0 $$\\mathcal {T}$$"],"prefix":"10.1007","author":[{"given":"Ian","family":"Mackie","sequence":"first","affiliation":[]},{"given":"Shinya","family":"Sato","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,2,21]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/11874683_8","volume-title":"Computer Science Logic","author":"S Alves","year":"2006","unstructured":"Alves, S., Florido, M., Fern\u00e1ndez, M., Mackie, I.: The power of linear functions. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 119\u2013134. Springer, Heidelberg (2006)"},{"issue":"11\u201313","key":"6_CR2","doi-asserted-by":"publisher","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."},{"issue":"6","key":"6_CR3","doi-asserted-by":"publisher","first-page":"763","DOI":"10.1017\/S0956796800001994","volume":"6","author":"A Asperti","year":"1996","unstructured":"Asperti, A., Giovannetti, C., Naletto, A.: The Bologna optimal higher-order machine. J. Funct. Program. 6(6), 763\u2013810 (1996)","journal-title":"J. Funct. Program."},{"key":"6_CR4","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"The Lambda calculus: its syntax and semantics","author":"HP Barendregt","year":"1984","unstructured":"Barendregt, H.P.: The Lambda calculus: its syntax and semantics. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland Publishing Company, Amsterdam (1984)"},{"issue":"3","key":"6_CR5","first-page":"427","volume":"9","author":"H Cirstea","year":"2001","unstructured":"Cirstea, H., Kirchner, C.: The rewriting calculus - Part I and II. Logic J. Interest Group Pure Appl. Logics 9(3), 427\u2013498 (2001)","journal-title":"Logic J. Interest Group Pure Appl. Logics"},{"key":"6_CR6","unstructured":"Lago, U.D.: The geometry of linear higher-order recursion. In: Panangaden, P., (ed.) Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, LICS 2005, pp. 366\u2013375. IEEE Computer Society Press, June 2005"},{"key":"6_CR7","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. 7. Cambridge University Press, Cambridge (1989)"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Gonthier, G., Abadi, M., L\u00e9vy, J.-J.: The geometry of optimal lambda reduction. In: Proceedings of the 19th ACM Symposium on Principles of Programming Languages (POPL 1992), pp. 15\u201326. ACM Press, January 1992","DOI":"10.1145\/143165.143172"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Lafont, Y.: Interaction nets. In: Proceedings of the 17th ACM Symposium on Principles of Programming Languages (POPL 1990), pp. 95\u2013108. ACM Press (1990)","DOI":"10.1145\/96709.96718"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Lamping, J.: An algorithm for optimal lambda calculus reduction. In: Proceedings of the 17th ACM Symposium on Principles of Programming Languages (POPL 1990), pp. 16\u201330. ACM Press, January 1990","DOI":"10.1145\/96709.96711"},{"key":"6_CR11","unstructured":"L\u00e9vy, J.-J.: Optimal reductions in the lambda calculus. In: Hindley, J.P., Seldin, J.R., (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 159\u2013191. Academic Press (1980)"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Lippi, S.: \n                    \n                      \n                    \n                    $$\\lambda $$\n                  -calculus left reduction with interaction nets. Math. Struct. Comput. Sci. 12(6) (2002)","DOI":"10.1017\/S0960129502003754"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Mackie, I.: YALE: yet another lambda evaluator based on interaction nets. In: Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming (ICFP 1998), pp. 117\u2013128. ACM Press, September 1998","DOI":"10.1145\/291251.289434"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-24452-0_3","volume-title":"Implementation and Application of Functional Languages","author":"I Mackie","year":"2011","unstructured":"Mackie, I.: An interaction net implementation of closed reduction. In: Scholz, S.-B., Chitil, O. (eds.) IFL 2008. LNCS, vol. 5836, pp. 43\u201359. Springer, Heidelberg (2011)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/11417170_28","volume-title":"Typed Lambda Calculi and Applications","author":"F-R Sinot","year":"2005","unstructured":"Sinot, F.-R.: Call-by-name and call-by-value as token-passing interaction nets. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 386\u2013400. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29604-3_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T14:00:24Z","timestamp":1578492024000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29604-3_6"}},"subtitle":["Declarative Pearl"],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296036","9783319296043"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29604-3_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"21 February 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}