More Web Proxy on the site http://driver.im/

Article

Free access

YALE: yet another lambda evaluator based on interaction nets

Author:

Ian MackieAuthors Info & Claims

ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming

Pages 117 - 128

https://doi.org/10.1145/289423.289434

Published: 29 September 1998 Publication History

Abstract

Interaction nets provide a graphical paradigm of computation based on net rewriting. They have proved most successful in understanding the dynamics of reduction in the λ-calculus, where the prime example is the implementation of optimal reduction for the λ-calculus (Lamping's algorithm), given by Gonthier, Abadi and Lévy. However, efficient implementations of optimal reduction have had to break away from the interaction net paradigm. In this paper we give a new efficient interaction net encoding of the λ-calculus which is not optimal, but overcomes the inefficiencies caused by the bookkeeping operations in the implementations of optimal reduction. We believe that this implementation of the λ-calculus could provide the basis for highly efficient implementations of functional languages.

References

[1]

Martin Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques L~vy. Explicit substitutions. Journal of Functional Programming, 1(4):375-416, October 1991.

[2]

Samson Abramsky. The lazy A-calculus. In David A. Turner, editor, Research Topics in Functional Programruing, chapter 4, pages 65-117. Addison Wesley, 1990.

Digital Library

[3]

Samson Abramsky. Computational Interpretations of Linear Logic. Theoretical Computer Science, 111:3-57, 1993.

Digital Library

[4]

Francisco Alberti. An abstract machine based on linear logic and explicit substitutions. Master's thesis, University of Birmingham, 1997.

[5]

Andrea Asperti, Cecilia Giovannetti, and Andrea Naletto. The bologna optimal higher-order machine. Journal of Functional Programming, 6(6):763- 810, November 1996.

[6]

Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, second, revised edition, 1984.

[7]

Vincent Danos and Laurent Regnier. Local and asynchronous beta-reduction (an analysis of Girard's execution formula). In Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science (LICS'93), pages 296-306. IEEE Computer Society Press, 1993.

[8]

Maribel Fernandez and Ian Mackie. A calculus for interaction nets, 1998. Available from http: //lix. pol yt e chnique, fr/~macki e.

[9]

Jean-Yves Girard. Linear Logic. Theoretical Computer Science, 50(1):1-102, 1987.

Digital Library

[10]

Jean-Yves Girard. Geometry of interaction 1: Interpretation of System F. In R. Ferro, C. Bonotto, S. Valentini, and A. Zanardo, editors, Logic Colloquium 88, Studies in Logic and the Foundations of Mathematics. North Holland Publishing Company, Amsterdam, August 1989.

[11]

Georges Gonthier, Martin Abadi, and Jean-Jacques L~vy. The geometry of optimal lambda reduction. In Proceedings of the 19th A CM Symposium on Principles of Programming Languages (POPL'9~), pages 15-26. ACM Press, January 1992.

Digital Library

[12]

SSren Holmstr5m. Linear functional programming. In T. Johnsson, Simon L. Peyton Jones, and K. Karlsson, editors, Proceedings of the Workshop on Implementation of Lazy Functional Languages, pages 13-32, 1988.

[13]

Yves Lafont. The Linear Abstract Machine. Theoretical Computer Science, 59(1,2):157-180, 1988.

Digital Library

[14]

Yves Lafont. Interaction nets. In Proceedings of the 17th A CM Symposium on Principles of Programming Language.s (POPL '90), pages 95-108. ACM Press, January 1990.

Digital Library

[15]

Yves Lafont. Interaction combinators. Information and Coraputation, 137(1):69-101, 1997.

Digital Library

[16]

John Lamping. An algorithm for optimal }ambda calculus reduction. In Proceedings of the 17th A CM Sympo-,ium on i)rinciples of Programming Languages, pages 16-30. ACM Press, January 1990.

Digital Library

[17]

Ian Madde. The Geometry of Implementation. PhD thesis, Department of Computing, Imperial College of Science, Technology and Medicine, September 1994.

[18]

lan Mackie. Lilac: A functional programming language based on linear logic. Journal of Functional Programruing, 4(4):395-433, October 1994.

[19]

Ian Macki~ The geometry of interaction machine. In Proceediny;s of the ~2nd A CM Symposium on Principles of ?;~o~ira~aming Languages (POPL '95), pages 198-208. ACM Press, January 1995.

[20]

Ion Mackic. Linear logic with boxes. In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS'98), pages 309-320. IEEE Computer Society Press, june 1998.

Digital Library

[21]

Ian Mack"e and Jorge Sousa Pinto. Compiling the ),-calculus into interaction combinators, January 1998. Available from http:/.lli x. polyte chnique, fr/~mackie.

[22]

Simon L. Feyton Jones. The Implementation of Funct:ional Programming Languages. Prentice Hall International, 1987.

Digital Library

[23]

Gmdon P'.otkin. LCF considered as a programming language. Theoretical Computer Science, 5(3):223-256, 1977.

[24]

Christopher P. Wadsworth. Semantics and Pragmatics .,~f ~he Lambda-Calculus. PhD thesis, Oxford University, 1972.

[25]

D'ax, id 'Wakeling. Linearity and Laziness. PhD thesis, Uni'~:m'sity of York, 1990.

Cited By

Grabmayer C(2024)From Compactifying Lambda-Letrec Terms to Recognizing Regular-Expression ProcessesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.408.2408(21-41)Online publication date: 1-Oct-2024
https://doi.org/10.4204/EPTCS.408.2
Fernandez MMackie I(2024)Hierarchical Higher-Order Port-Graphs: A Rewriting-Based Modelling LanguageProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678238(1-14)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678238
Kesner D(2022)A fine-grained computational interpretation of Girard’s intuitionistic proof-netsProceedings of the ACM on Programming Languages10.1145/34986696:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498669
Show More Cited By

Index Terms

YALE: yet another lambda evaluator based on interaction nets
1. Mathematics of computing
2. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types

Recommendations

YALE: yet another lambda evaluator based on interaction nets

Interaction nets provide a graphical paradigm of computation based on net rewriting. They have proved most successful in understanding the dynamics of reduction in the λ-calculus, where the prime example is the implementation of optimal reduction ...
Intuitionistic Trilattice Logics

We take up a suggestion by Odintsov (2009, Studia Logica, 91, 407–428) and define intuitionistic variants of certain logics arising from the trilattice SIXTEEN₃ introduced in Shramko and Wansing (2005, Journal of Philosophical Logic, 34, 121–153 and ...
Proving Isomorphism of First-Order Logic Proof Systems in HOL

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming

September 1998

351 pages

ISBN:1581130244

DOI:10.1145/289423

Chairmen:
Matthias Felleisen
Rice Univ., Houston, TX
,
Paul Hudak
Yale Univ., New Haven, CT
,
Christian Queinnec
Univ. Paris 6; and INRIA

ACM SIGPLAN Notices Volume 34, Issue 1
Jan. 1999
357 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/291251
Chairmen:
Matthias Felleisen
Rice Univ.
,
Paul Hudak
Yale Univ.
,
Editor:
A. Michael Berman
Issue’s Table of Contents

Copyright © 1998 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 September 1998

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

ICFP98

Sponsor:

SIGPLAN

ICFP98: 1998 International Conference on Functional Programming

September 26 - 29, 1998

Maryland, Baltimore, USA

Acceptance Rates

ICFP '98 Paper Acceptance Rate 30 of 77 submissions, 39%;

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

37
Total Citations
View Citations
911
Total Downloads

Downloads (Last 12 months)194
Downloads (Last 6 weeks)32

Reflects downloads up to 17 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Grabmayer C(2024)From Compactifying Lambda-Letrec Terms to Recognizing Regular-Expression ProcessesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.408.2408(21-41)Online publication date: 1-Oct-2024
https://doi.org/10.4204/EPTCS.408.2
Fernandez MMackie I(2024)Hierarchical Higher-Order Port-Graphs: A Rewriting-Based Modelling LanguageProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678238(1-14)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678238
Kesner D(2022)A fine-grained computational interpretation of Girard’s intuitionistic proof-netsProceedings of the ACM on Programming Languages10.1145/34986696:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498669
Lippi S(2019)Universal Hard Interaction for Clockless ComputationFundamenta Informaticae10.5555/2362676.236268591:2(357-394)Online publication date: 4-Jan-2019
https://dl.acm.org/doi/10.5555/2362676.2362685
Lippi S(2019)Universal Hard Interaction for Clockless ComputationFundamenta Informaticae10.5555/1549637.154966191:2(357-394)Online publication date: 4-Jan-2019
https://dl.acm.org/doi/10.5555/1549637.1549661
Sinot F(2019)Token-Passing NetsElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2005.09.027135:3(129-139)Online publication date: 5-Jan-2019
https://dl.acm.org/doi/10.1016/j.entcs.2005.09.027
Mackie I(2019)Interaction nets for linear logicTheoretical Computer Science10.1016/S0304-3975(00)00198-5247:1-2(83-140)Online publication date: 5-Jan-2019
https://dl.acm.org/doi/10.1016/S0304-3975%2800%2900198-5
YASEN AUEDA K(2018)Name Binding is Easy with HypergraphsIEICE Transactions on Information and Systems10.1587/transinf.2017EDP7257E101.D:4(1126-1140)Online publication date: 2018
https://doi.org/10.1587/transinf.2017EDP7257
Lippi S(2018)The graphical Krivine machineHigher-Order and Symbolic Computation10.1007/s10990-007-9011-320:3(295-318)Online publication date: 15-Dec-2018
https://dl.acm.org/doi/10.1007/s10990-007-9011-3
Mackie ISato S(2016)An Interaction Net Encoding of Gödel’s System $$\mathcal {T}$$Functional and Logic Programming10.1007/978-3-319-29604-3_6(80-93)Online publication date: 21-Feb-2016
https://doi.org/10.1007/978-3-319-29604-3_6
Show More Cited By

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 Publication

Media

Figures

Other

Tables

View Table of Contents