{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:08Z","timestamp":1747173428381,"version":"3.40.5"},"reference-count":42,"publisher":"Cambridge University Press (CUP)","issue":"9","license":[{"start":{"date-parts":[[2019,4,8]],"date-time":"2019-04-08T00:00:00Z","timestamp":1554681600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2019,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we propose and explore a new approach to abstract machines and optimal reduction via streams, infinite sequences of elements. We first define a sequential abstract machine capable of performing directed virtual reduction (DVR) and then we extend it to its parallel version, whose equivalence is explained through the properties of DVR itself. The result is a formal definition of the <jats:italic>\u03bb<\/jats:italic>-calculus interpreter called Parallel Environment for Lambda Calculus Reduction (PELCR), a software for <jats:italic>\u03bb<\/jats:italic>-calculus reduction based on the Geometry of Interaction. In particular, we describe PELCR as a stream-processing abstract machine, which in principle can also be applied to infinite streams.<\/jats:p>","DOI":"10.1017\/s096012951900001x","type":"journal-article","created":{"date-parts":[[2019,4,8]],"date-time":"2019-04-08T06:01:46Z","timestamp":1554703306000},"page":"1379-1410","source":"Crossref","is-referenced-by-count":0,"title":["Abstract machines, optimal reduction, and streams"],"prefix":"10.1017","volume":"29","author":[{"given":"Anna Chiara","family":"Lai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9016-074X","authenticated-orcid":false,"given":"Marco","family":"Pedicini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mario","family":"Piazza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2019,4,8]]},"reference":[{"key":"S096012951900001X_ref17","first-page":"34","volume-title":"Proceedings of Conference on Functional Programming and Computer Architecture","volume":"274","author":"Fairbairn","year":"1987"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref42","DOI":"10.1016\/j.jcss.2010.06.012"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref38","DOI":"10.1017\/S0960129504004517"},{"volume-title":"Proceedings of the 2nd ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming \u2013 PPDP \u201900","year":"2000","author":"Pedicini","key":"S096012951900001X_ref33"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref36","DOI":"10.1007\/3-540-45413-6_30"},{"key":"S096012951900001X_ref9","first-page":"19","article-title":"Typing a core binary-field arithmetic in a light logic","volume":"7177","author":"Cesena","year":"2012","journal-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref16","DOI":"10.1017\/CBO9780511629150.016"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref3","DOI":"10.1007\/s002000050083"},{"volume-title":"Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications","year":"2005","author":"Charles","key":"S096012951900001X_ref10"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref35","DOI":"10.1145\/1243996.1243997"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref12","DOI":"10.1016\/0304-3975(91)90230-Y"},{"volume-title":"Preproceedings of the 15th Symposium on Trends in. Functional Programming","year":"2014","author":"Pedicini","key":"S096012951900001X_ref31"},{"unstructured":"Pedicini, M. (1998). Ex\u00e9cution et Programmes. PhD thesis, Universit\u00e9 Paris VII.","key":"S096012951900001X_ref30"},{"key":"S096012951900001X_ref27","first-page":"159","article-title":"Optimal reductions in the lambda-calculus","author":"L\u00e9vy","year":"1980","journal-title":"To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism"},{"unstructured":"L\u00e9vy, J.-J. (1978). R\u00e9ductions Correctes et Optimales Dans le Lambda-Calcul. PhD thesis, Universit\u00e9 Paris VII.","key":"S096012951900001X_ref26"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref25","DOI":"10.1142\/3645"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref34","DOI":"10.1007\/3-540-45706-2_89"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref8","DOI":"10.1016\/j.scico.2015.04.001"},{"key":"S096012951900001X_ref1","first-page":"363","volume-title":"Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, Gothenburg, Sweden, September 1\u20133, 2014","author":"Accattoli","year":"2014"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref4","DOI":"10.1017\/S0956796800001994"},{"key":"S096012951900001X_ref7","first-page":"38","article-title":"Can a light typing discipline be compatible with an efficient implementation of finite fields inversion?","volume":"8552","author":"Canavese","year":"2014","journal-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref2","DOI":"10.1109\/HPCS.2018.00085"},{"unstructured":"Muroya, K. and Ghica, D. R. (2017). The dynamic geometry of interaction machine: a call-by-need graph rewriter. In: Computer science logic 2017, volume 82 of LIPIcs. Leibniz Int. Proc. Inform., Art. No. 32, 15. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern.","key":"S096012951900001X_ref29"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref39","DOI":"10.1016\/j.tcs.2005.06.019"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref41","DOI":"10.1145\/79173.79181"},{"volume-title":"Introduction to Combinators and \u03bb-Calculus","year":"1986","author":"Hindley","key":"S096012951900001X_ref22"},{"key":"S096012951900001X_ref6","first-page":"1","article-title":"Elementary complexity and geometry of interaction","volume":"45","author":"Baillot","year":"2001","journal-title":"Fund. Inform."},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref20","DOI":"10.1017\/CBO9780511629150.017"},{"key":"S096012951900001X_ref21","first-page":"15","volume-title":"Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Gonthier","year":"1992"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref13","DOI":"10.1109\/LICS.2015.58"},{"key":"S096012951900001X_ref18","first-page":"221","volume-title":"Logic Colloquium \u201988 (Padova, 1988)","volume":"127","author":"Girard","year":"1989"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref15","DOI":"10.1109\/LICS.1993.287578"},{"key":"S096012951900001X_ref28","first-page":"198","volume-title":"Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Mackie","year":"1995"},{"key":"S096012951900001X_ref23","first-page":"16","volume-title":"Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Lamping","year":"1989"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref19","DOI":"10.1007\/3-540-52335-9_49"},{"key":"S096012951900001X_ref40","first-page":"1","article-title":"Geometry of resource interaction and Taylor-Ehrhard-Regnier expansion: A minimalist approach","author":"Solieri","year":"2016","journal-title":"Mathematical Structures in Computer Science"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref11","DOI":"10.1017\/CBO9781139173018"},{"key":"S096012951900001X_ref5","volume-title":"The Optimal Implementation of Functional Programming languages","volume":"45","author":"Asperti","year":"1998"},{"unstructured":"Regnier, L. (1992). Lambda-calcul et r\u00e9seaux. PhD thesis, Universit\u00e9 Paris VII.","key":"S096012951900001X_ref37"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref14","DOI":"10.1007\/3-540-63172-0_33"},{"key":"S096012951900001X_ref32","first-page":"1","article-title":"K\u00e1lmar elementary complexity and von Neumann algebras","volume":"28","author":"Pedicini","year":"2018","journal-title":"Panamerican Mathematical Journal"},{"doi-asserted-by":"publisher","key":"S096012951900001X_ref24","DOI":"10.1093\/comjnl\/6.4.308"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S096012951900001X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,11]],"date-time":"2019-11-11T06:05:06Z","timestamp":1573452306000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S096012951900001X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4,8]]},"references-count":42,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2019,10]]}},"alternative-id":["S096012951900001X"],"URL":"https:\/\/doi.org\/10.1017\/s096012951900001x","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2019,4,8]]}}}