research-article

Open access

The (In)Efficiency of interaction

Authors:

Beniamino Accattoli,

Gabriele VanoniAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue POPL

Article No.: 51, Pages 1 - 33

https://doi.org/10.1145/3434332

Published: 04 January 2021 Publication History

Abstract

Evaluating higher-order functional programs through abstract machines inspired by the geometry of the interaction is known to induce space efficiencies, the price being time performances often poorer than those obtainable with traditional, environment-based, abstract machines. Although families of lambda-terms for which the former is exponentially less efficient than the latter do exist, it is currently unknown how general this phenomenon is, and how far the inefficiencies can go, in the worst case. We answer these questions formulating four different well-known abstract machines inside a common definitional framework, this way being able to give sharp results about the relative time efficiencies. We also prove that non-idempotent intersection type theories are able to precisely reflect the time performances of the interactive abstract machine, this way showing that its time-inefficiency ultimately descends from the presence of higher-order types.

References

[1]

Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. 2000. Full Abstraction for PCF. Inf. Comput. 163, 2 ( 2000 ), 409-470. https://doi.org/10.1006/inco. 2000.2930

Digital Library

[2]

Beniamino Accattoli. 2017. (In)Eficiency and Reasonable Cost Models. In 12th Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2017, Brasília, Brazil, September 23-24, 2017 (Electronic Notes in Theoretical Computer Science, Vol. 338 ). Elsevier, 23-43. https://doi.org/10.1016/j.entcs. 2018. 10.003

[3]

Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. 2014. Distilling abstract machines. In Proceedings of the 19th ACM SIGPLAN international conference on Functional progranitarmming, Gothenburg, Sweden, September 1-3, 2014, Johan Jeuring and Manuel M. T. Chakravarty (Eds.). ACM, 363-376. https://doi.org/10.1145/2628136.2628154

Digital Library

[4]

Beniamino Accattoli and Bruno Barras. 2017. Environments and the complexity of abstract machines. In Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09-11, 2017, Wim Vanhoof and Brigitte Pientka (Eds.). ACM, 4-16. https://doi.org/10.1145/3131851.3131855

Digital Library

[5]

Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, and Claudio Sacerdoti Coen. 2019a. Crumbling Abstract Machines. In Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019, Porto, Portugal, October 7-9, 2019, Ekaterina Komendantskaya (Ed.). ACM, 4 : 1-4 : 15. https://doi.org/10.1145/3354166.3354169

Digital Library

[6]

Beniamino Accattoli and Ugo Dal Lago. 2012. On the Invariance of the Unitary Cost Model for Head Reduction. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12), RTA 2012, May 28-June 2, 2012, Nagoya, Japan (LIPIcs, Vol. 15 ), Ashish Tiwari (Ed.). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 22-37. https: //doi.org/10.4230/LIPIcs.RTA. 2012.22

[7]

Beniamino Accattoli and Ugo Dal Lago. 2016. (Leftmost-Outermost) Beta Reduction is Invariant, Indeed. Logical Methods in Computer Science 12, 1 ( 2016 ). https://doi.org/10.2168/LMCS-12 ( 1 :4) 2016

[8]

Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. 2020a. The (In)Eficiency of Interaction. Technical Report. https://arxiv.org/abs/ 2010.12988.

[9]

Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. 2020b. The Machinery of Interaction. In PPDP '20: 22nd International Symposium on Principles and Practice of Declarative Programming, Bologna, Italy, 9-10 September, 2020. ACM, 4 : 1-4 : 15. https://doi.org/10.1145/3414080.3414108

Digital Library

[10]

Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. 2020c. Tight typings and split bounds, fully developed. J. Funct. Program. 30 ( 2020 ), e14. https://doi.org/10.1017/S095679682000012X

[11]

Beniamino Accattoli and Giulio Guerrieri. 2018. Types of Fireballs. In Programming Languages and Systems-16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings (Lecture Notes in Computer Science, Vol. 11275 ), Sukyoung Ryu (Ed.). Springer, 45-66. https://doi.org/10.1007/978-3-030-02768-1_3

[12]

Beniamino Accattoli and Giulio Guerrieri. 2019. Abstract machines for Open Call-by-Value. Sci. Comput. Program. 184 ( 2019 ). https://doi.org/10.1016/j.scico. 2019. 03.002

[13]

Beniamino Accattoli, Giulio Guerrieri, and Maico Leberle. 2019b. Types by Need. In Programming Languages and Systems-28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings (Lecture Notes in Computer Science, Vol. 11423 ). Springer, 410-439. https://doi.org/10.1007/978-3-030-17184-1_15

[14]

Federico Aschieri. 2017. Game Semantics and the Geometry of Backtracking: a New Complexity Analysis of Interaction. J. Symb. Log. 82, 2 ( 2017 ), 672-708. https://doi.org/10.1017/jsl. 2016.48

[15]

Andrea Asperti, Vincent Danos, Cosimo Laneve, and Laurent Regnier. 1994. Paths in the lambda-calculus. In Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), Paris, France, July 4-7, 1994. IEEE Computer Society, 426-436. https://doi.org/10.1109/LICS. 1994.316048

[16]

Patrick Baillot. 1999. Approches dynamiques en sémantique de la logique lineaire: jeux et géométrie de l'interaction. PhD Thesis. Universite Aix-Marseille 2.

[17]

Patrick Baillot, Paolo Coppola, and Ugo Dal Lago. 2011. Light logics and optimal reduction: Completeness and complexity. Inf. Comput. 209, 2 ( 2011 ), 118-142. https://doi.org/10.1016/j.ic. 2010. 10.002

Digital Library

[18]

Hendrik Pieter Barendregt. 1984. The lambda calculus: its syntax and semantics. North-Holland.

[19]

Daniil Berezun and Neil D. Jones. 2017. Compiling untyped lambda calculus to lower-level code by game semantics and partial evaluation (invited paper). In Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2017, Paris, France, January 18-20, 2017, Ulrik Pagh Schultz and Jeremy Yallop (Eds.). ACM, 1-11.

Digital Library

[20]

Alexis Bernadet and Stéphane Graham-Lengrand. 2013. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science 9, 4 ( 2013 ). https://doi.org/10.2168/LMCS-9( 4 :3) 2013

[21]

Guy E. Blelloch and John Greiner. 1995. Parallelism in Sequential Functional Languages. In Proceedings of the seventh international conference on Functional programming languages and computer architecture, FPCA 1995, La Jolla, California, USA, June 25-28, 1995. ACM, 226-237. https://doi.org/10.1145/224164.224210

Digital Library

[22]

William Blum. 2020. Evaluating lambda terms with traversals. Theor. Comput. Sci. 802 ( 2020 ), 77-104. https://doi.org/10. 1016/j.tcs. 2019. 08.035

[23]

Antonio Bucciarelli, Delia Kesner, Alejandro Ríos, and Andrés Viso. 2020. The Bang Calculus Revisited. In Functional and Logic Programming-15th International Symposium, FLOPS 2020, Akita, Japan, September 14-16, 2020, Proceedings (Lecture Notes in Computer Science, Vol. 12073 ), Keisuke Nakano and Konstantinos Sagonas (Eds.). Springer, 13-32. https://doi.org/10.1007/978-3-030-59025-3_2

[24]

Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. 2017. Non-idempotent intersection types for the Lambda-Calculus. Logic Journal of the IGPL 25, 4 ( 2017 ), 431-464. https://doi.org/10.1093/jigpal/jzx018

[25]

Pierre Clairambault. 2011. Estimation of the Length of Interactions in Arena Game Semantics. In Foundations of Software Science and Computational Structures-14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings (Lecture Notes in Computer Science, Vol. 6604 ), Martin Hofmann (Ed.). Springer, 335-349. https://doi.org/10.1007/978-3-642-19805-2_23

[26]

Pierre Clairambault. 2015. Bounding linear head reduction and visible interaction through skeletons. Log. Methods Comput. Sci. 11, 2 ( 2015 ). https://doi.org/10.2168/LMCS-11 ( 2 :6) 2015

[27]

Mario Coppo and Mariangiola Dezani-Ciancaglini. 1978. A new type assignment for λ-terms. Arch. Math. Log. 19, 1 ( 1978 ), 139-156. https://doi.org/10.1007/BF02011875

[28]

Mario Coppo and Mariangiola Dezani-Ciancaglini. 1980. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic 21, 4 ( 1980 ), 685-693. https://doi.org/10.1305/ndjfl/1093883253

[29]

Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. 1980. Principal Type Schemes and Lambda-calculus Semantics. In To H.B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism. Academic Press, 535-560. http://www.di.unito.it/~dezani/papers/CDV80.pdf

[30]

Pierre-Louis Curien and Hugo Herbelin. 1998. Computing with Abstract Böhm Trees. In Third Fuji International Symposium on Functional and Logic Programming, FLOPS 1998, Kyoto, Japan, Apil 2-4, 1998, Masahiko Sato and Yoshihito Toyama (Eds.). World Scientific, Singapore, 20-39.

[31]

Pierre-Louis Curien and Hugo Herbelin. 2007. Abstract machines for dialogue games. ( 2007 ). http://arxiv.org/abs/0706.2544

[32]

Ugo Dal Lago, Claudia Faggian, Ichiro Hasuo, and Akira Yoshimizu. 2014. The geometry of synchronization. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14-18, 2014, Thomas A. Henzinger and Dale Miller (Eds.). ACM, 35 : 1-35 : 10. https://doi.org/10.1145/2603088.2603154

Digital Library

[33]

Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu. 2015. Parallelism and Synchronization in an Infinitary Context. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015. IEEE Computer Society, 559-572. https://doi.org/10.1109/LICS. 2015.58

Digital Library

[34]

Ugo Dal Lago and Ulrich Schöpp. 2010. Functional Programming in Sublinear Space. In Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings (Lecture Notes in Computer Science, Vol. 6012 ), Andrew D. Gordon (Ed.). Springer, 205-225. https://doi.org/10.1007/978-3-642-11957-6_12

Digital Library

[35]

Ugo Dal Lago and Ulrich Schöpp. 2016. Computation by interaction for space-bounded functional programming. Information and Computation 248 ( 2016 ), 150-194. https://doi.org/10.1016/j.ic. 2015. 04.006

Digital Library

[36]

Ugo Dal Lago, Ryo Tanaka, and Akira Yoshimizu. 2017. The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. IEEE Computer Society, 1-12. https://doi.org/10.1109/LICS. 2017.8005112

[37]

Ugo Dal Lago and Margherita Zorzi. 2014. Wave-Style Token Machines and Quantum Lambda Calculi. In Proceedings Third International Workshop on Linearity, LINEARITY 2014, Vienna, Austria, 13th July, 2014 (EPTCS, Vol. 176 ), Sandra Alves and Iliano Cervesato (Eds.). 64-78. https://doi.org/10.4204/EPTCS.176.6

[38]

Vincent Danos, Hugo Herbelin, and Laurent Regnier. 1996. Game Semantics & Abstract Machines. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996. IEEE Computer Society, 394-405. https://doi.org/10.1109/LICS. 1996.561456

[39]

Vincent Danos and Laurent Regnier. 1993. Local and asynchronous beta-reduction (an analysis of Girard's execution formula). In Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), Montreal, Canada, June 19-23, 1993. IEEE Computer Society, 296-306. https://doi.org/10.1109/LICS. 1993.287578

[40]

Vincent Danos and Laurent Regnier. 1995. Proof-Nets and the Hilbert Space. In Proceedings of the Workshop on Advances in Linear Logic. Cambridge University Press, USA, 307-328.

Digital Library

[41]

Vincent Danos and Laurent Regnier. 1999. Reversible, irreversible and optimal lambda-machines. Theoretical Computer Science 227, 1 ( 1999 ), 79-97. https://doi.org/10.1016/S0304-3975 ( 99 ) 00049-3

Digital Library

[42]

Vincent Danos and Laurent Regnier. 2004. Head Linear Reduction. Technical Report.

[43]

Daniel de Carvalho. 2007. Sémantiques de la logique linéaire et temps de calcul. Thèse de Doctorat. Université Aix-Marseille II.

[44]

Daniel de Carvalho. 2018. Execution time of λ-terms via denotational semantics and intersection types. Math. Str. in Comput. Sci. 28, 7 ( 2018 ), 1169-1203. https://doi.org/10.1017/S0960129516000396

[45]

Daniel de Carvalho, Michele Pagani, and Lorenzo Tortora de Falco. 2011. A semantic measure of the execution time in linear logic. Theoretical Computer Science 412, 20 ( 2011 ), 1884-1902. https://doi.org/10.1016/j.tcs. 2010. 12.017

Digital Library

[46]

Maribel Fernández and Ian Mackie. 2002. Call-by-Value lambda-Graph Rewriting Without Rewriting. In Graph Transformation, First International Conference, ICGT 2002, Barcelona, Spain, October 7-12, 2002, Proceedings (Lecture Notes in Computer Science, Vol. 2505 ), Andrea Corradini, Hartmut Ehrig, Hans-Jörg Kreowski, and Grzegorz Rozenberg (Eds.). Springer, 75-89. https://doi.org/10.1007/3-540-45832-8_8

[47]

Philippa Gardner. 1994. Discovering Needed Reductions Using Type Theory. In Theoretical Aspects of Computer Software (TACS '94) (Lecture Notes in Computer Science, Vol. 789 ). 555-574. https://doi.org/10.1007/3-540-57887-0_115

[48]

Dan R. Ghica. 2007. Geometry of Synthesis: A Structured Approach to VLSI Design. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, Martin Hofmann and Matthias Felleisen (Eds.). ACM, 363-375. https://doi.org/10.1145/1190216.1190269

Digital Library

[49]

Dan R. Ghica and Alex I. Smith. 2010. Geometry of Synthesis II: From Games to Delay-Insensitive Circuits. In Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2010, Ottawa, Ontario, Canada, May 6-10, 2010 (Electronic Notes in Theoretical Computer Science, Vol. 265 ), Michael W. Mislove and Peter Selinger (Eds.). Elsevier, 301-324. https://doi.org/10.1016/j.entcs. 2010. 08.018

Digital Library

[50]

Jean-Yves Girard. 1987. Linear logic. Theoretical Computer Science 50, 1 ( 1987 ), 1-101. https://doi.org/10.1016/ 0304-3975 ( 87 ) 90045-4

Digital Library

[51]

Jean-Yves Girard. 1989. Geometry of Interaction 1: Interpretation of System F. In Studies in Logic and the Foundations of Mathematics, R. Ferro, C. Bonotto, S. Valentini, and A. Zanardo (Eds.). Vol. 127. Elsevier, 221-260.

[52]

Naohiko Hoshino, Koko Muroya, and Ichiro Hasuo. 2014. Memoryful geometry of interaction: from coalgebraic components to algebraic efects. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14-18, 2014, Thomas A. Henzinger and Dale Miller (Eds.). ACM, 52 : 1-52 : 10. https://doi.org/10.1145/2603088.2603124

Digital Library

[53]

J. M. E. Hyland and C.-H. Luke Ong. 2000. On Full Abstraction for PCF: I, II, and III. Inf. Comput. 163, 2 ( 2000 ), 285-408. https://doi.org/10.1006/inco. 2000.2917

Digital Library

[54]

Delia Kesner and Pierre Vial. 2020. Consuming and Persistent Types for Classical Logic. In LICS ' 20 : 35th Annual ACM /IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller (Eds.). ACM, 619-632. https://doi.org/10.1145/3373718.3394774

Digital Library

[55]

Assaf J. Kfoury. 2000. A linearization of the Lambda-calculus and consequences. Journal of Logic and Computation 10, 3 ( 2000 ), 411-436. https://doi.org/10.1093/logcom/10.3. 411

[56]

Neelakantan R. Krishnaswami, Nick Benton, and Jan Hofmann. 2012. Higher-order functional reactive programming in bounded space. In Proc. of POPL 2012, John Field and Michael Hicks (Eds.). ACM, 45-58. https://doi.org/10.1145/2103656. 2103665

Digital Library

[57]

Jean-Louis Krivine. 1993. Lambda-calculus, types and models. Masson.

[58]

Jean-Louis Krivine. 2007. A Call-by-name Lambda-calculus Machine. Higher Order Symbol. Comput. 20, 3 ( 2007 ), 199-207. https://doi.org/10.1007/s10990-007-9018-9

Digital Library

[59]

Olivier Laurent. 2001. A Token Machine for Full Geometry of Interaction. In Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Krakow, Poland, May 2-5, 2001, Proceedings (Lecture Notes in Computer Science, Vol. 2044 ), Samson Abramsky (Ed.). Springer, 283-297. https://doi.org/10.1007/3-540-45413-6_23

[60]

Jean-Jacques Lévy. 1978. Réductions correctes et optimales dans le lambda-calcul. PhD Thesis. Université Paris 7.

[61]

Ian Mackie. 1995. The Geometry of Interaction Machine. In Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, Ron K. Cytron and Peter Lee (Eds.). ACM Press, 198-208. https://doi.org/10.1145/199448.199483

Digital Library

[62]

Ian Mackie. 2017. A Geometry of Interaction Machine for Gödel's System T. In Logic, Language, Information, and Computation-24th International Workshop, WoLLIC 2017, London, UK, July 18-21, 2017, Proceedings (Lecture Notes in Computer Science, Vol. 10388 ), Juliette Kennedy and Ruy J. G. B. de Queiroz (Eds.). Springer, 229-241. https://doi.org/10.1007/978-3-662-55386-2_16

[63]

Damiano Mazza. 2015. Simple Parsimonious Types and Logarithmic Space. In 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany (LIPIcs, Vol. 41 ), Stephan Kreutzer (Ed.). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 24-40. https://doi.org/10.4230/LIPIcs.CSL. 2015.24

[64]

Damiano Mazza, Luc Pellissier, and Pierre Vial. 2018. Polyadic approximations, fibrations and intersection types. Proc. ACM Program. Lang. 2, POPL ( 2018 ), 6 : 1-6 : 28. https://doi.org/10.1145/3158094

Digital Library

[65]

Damiano Mazza and Kazushige Terui. 2015. Parsimonious Types and Non-uniform Computation. In Automata, Languages, and Programming-42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II (Lecture Notes in Computer Science, Vol. 9135 ), Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann (Eds.). Springer, 350-361. https://doi.org/10.1007/978-3-662-47666-6_28

Digital Library

[66]

Robin Milner. 1977. Fully Abstract Models of Typed lambda-Calculi. Theor. Comput. Sci. 4, 1 ( 1977 ), 1-22. https: //doi.org/10.1016/ 0304-3975 ( 77 ) 90053-6

[67]

Koko Muroya and Dan R. Ghica. 2017. The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter. In 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, August 20-24, 2017, Stockholm, Sweden (LIPIcs, Vol. 82 ), Valentin Goranko and Mads Dam (Eds.). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 32 : 1-32 : 15. https: //doi.org/10.4230/LIPIcs.CSL. 2017.32

[68]

Koko Muroya and Dan R. Ghica. 2019. The Dynamic Geometry of Interaction Machine: A Token-Guided Graph Rewriter. Log. Methods Comput. Sci. 15, 4 ( 2019 ). https://lmcs.episciences. org/5882

[69]

Peter Møller Neergaard and Harry G. Mairson. 2004. Types, potency, and idempotency: why nonlinearity and amnesia make a type system work. In Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, ICFP 2004, Snow Bird, UT, USA, September 19-21, 2004, Chris Okasaki and Kathleen Fisher (Eds.). ACM, 138-149. https: //doi.org/10.1145/1016850.1016871

Digital Library

[70]

C.-H. Luke Ong. 2006. On Model-Checking Trees Generated by Higher-Order Recursion Schemes. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006 ), 12-15 August 2006, Seattle, WA, USA, Proceedings. IEEE Computer Society, 81-90. https://doi.org/10.1109/LICS. 2006.38

Digital Library

[71]

Marco Pedicini and Francesco Quaglia. 2007. PELCR: Parallel environment for optimal lambda-calculus reduction. ACM Trans. Comput. Log. 8, 3 ( 2007 ), 14. https://doi.org/10.1145/1243996.1243997

Digital Library

[72]

Jorge Sousa Pinto. 2001. Parallel Implementation Models for the lambda-Calculus Using the Geometry of Interaction. In Proc. of TLCA 2001 (LNCS, Vol. 2044 ), Samson Abramsky (Ed.). Springer, 385-399. https://doi.org/10.1007/3-540-45413-6_30

[73]

Garrel Pottinger. 1980. A Type Assignment for The Strongly Normalizable λ-terms. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J.P. Seldin and J.R. Hindley (Eds.). Academic Press, 561-578.

[74]

David Sands, Jörgen Gustavsson, and Andrew Moran. 2002. Lambda Calculi and Linear Speedups. In The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones [on occasion of his 60th birthday] (Lecture Notes in Computer Science, Vol. 2566 ), Torben Æ. Mogensen, David A. Schmidt, and Ivan Hal Sudborough (Eds.). Springer, 60-84. https://doi.org/10.1007/3-540-36377-7_4

[75]

Ulrich Schopp. 2007. Stratified Bounded Afine Logic for Logarithmic Space. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007 ), 10-12 July 2007, Wroclaw, Poland, Proceedings. IEEE Computer Society, 411-420. https://doi.org/10. 1109/LICS. 2007.45

Digital Library

[76]

Ulrich Schöpp. 2014. On the Relation of Interaction Semantics to Continuations and Defunctionalization. Logical Methods in Computer Science 10, 4 ( 2014 ). https://doi.org/10.2168/LMCS-10 ( 4 :10) 2014

[77]

Ulrich Schöpp. 2015. From Call-by-Value to Interaction by Typed Closure Conversion. In Programming Languages and Systems-13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30-December 2, 2015, Proceedings (Lecture Notes in Computer Science, Vol. 9458 ), Xinyu Feng and Sungwoo Park (Eds.). Springer, 251-270. https://doi.org/10.1007/978-3-319-26529-2_14

[78]

Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. 2017. Generalised species of rigid resource terms. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. IEEE Computer Society, 1-12. https://doi.org/10.1109/LICS. 2017.8005093

Cited By

Faggian CPautasso DVanoni G(2024)Higher Order Bayesian Networks, ExactlyProceedings of the ACM on Programming Languages10.1145/36329268:POPL(2514-2546)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632926
Cimini M(2023)Towards the Complexity Analysis of Programming Language Proof MethodsTheoretical Aspects of Computing – ICTAC 202310.1007/978-3-031-47963-2_8(100-118)Online publication date: 4-Dec-2023
https://dl.acm.org/doi/10.1007/978-3-031-47963-2_8
Accattoli BGuerrieri G(2022)The theory of call-by-value solvabilityProceedings of the ACM on Programming Languages10.1145/35476526:ICFP(855-885)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547652
Show More Cited By

Index Terms

The (In)Efficiency of interaction
1. Theory of computation
  1. Models of computation
    1. Abstract machines
    2. Computability
      1. Lambda calculus

Recommendations

The Machinery of Interaction
PPDP '20: Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming

This paper revisits the Interaction Abstract Machine (IAM), a machine based on Girard’s Geometry of Interaction, introduced by Mackie and Danos & Regnier. It is an unusual machine, not relying on environments, presented on linear logic proof nets, and ...
Computation in focused intuitionistic logic
PPDP '15: Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming

We investigate the control of evaluation strategies in a variant of the Λ-calculus derived through the Curry-Howard correspondence from LJF, a sequent calculus for intuitionistic logic implementing the focusing technique. The proof theory of focused ...
Distilling abstract machines
ICFP '14: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming

It is well-known that many environment-based abstract machines can be seen as strategies in lambda calculi with explicit substitutions (ES). Recently, graphical syntaxes and linear logic led to the linear substitution calculus (LSC), a new approach to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 5, Issue POPL

January 2021

1789 pages

EISSN:2475-1421

DOI:10.1145/3445980

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 January 2021

Published in PACMPL Volume 5, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
737
Total Downloads

Downloads (Last 12 months)228
Downloads (Last 6 weeks)33

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Faggian CPautasso DVanoni G(2024)Higher Order Bayesian Networks, ExactlyProceedings of the ACM on Programming Languages10.1145/36329268:POPL(2514-2546)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632926
Cimini M(2023)Towards the Complexity Analysis of Programming Language Proof MethodsTheoretical Aspects of Computing – ICTAC 202310.1007/978-3-031-47963-2_8(100-118)Online publication date: 4-Dec-2023
https://dl.acm.org/doi/10.1007/978-3-031-47963-2_8
Accattoli BGuerrieri G(2022)The theory of call-by-value solvabilityProceedings of the ACM on Programming Languages10.1145/35476526:ICFP(855-885)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547652
Accattoli BDal Lago UVanoni G(2022)Multi types and reasonable spaceProceedings of the ACM on Programming Languages10.1145/35476506:ICFP(799-825)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547650
Accattoli BDal Lago UVanoni G(2022)Reasonable Space for the λ-Calculus, LogarithmicallyProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533362(1-13)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3533362
Accattoli BLago UVanoni GGorla D(2021)The space of interactionProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470726(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470726
Laird JGorla D(2021)A compositional cost model for the λ-calculusProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470567(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470567

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents