Interaction Nets

Projects

• HVM/Bend website, orga, repo, discord
  • interaction combinators as a backend of a Python/Haskell-like language
  • focus on efficient, parallel, and optimal reduction of the lambda calculus without oracle
• Vine website, orga, repo, discord
  • interaction nets as a backend of a Rust-like language
  • focus on concurrency and interoperation between functional and imperative patterns
• Inpla repo
  • focus on custom interaction rules and interaction calculus
• ∆-Nets website, repo
  • interactive translator from lambda calculus to ∆-Nets (variation of interaction nets)
• inet-forth repo
  • focus on custom interaction rules and interaction calculus in forth
• optiscope repo
  • efficient implementation of lambdascope
• GoI-Visualizer website, repo
  • interactive translator from lambda calculus to an interaction net-like token-passing encoding (GoI)
  • focus on enforcing reduction strategies by various applicator-token interactions

Blog Posts

• 20XX: Buliga, Graphic Lambda Calculus, Universality of Interaction Combinators, more
• 20XX: Taelin, Symmetric Interaction Calculus, Optimal Evaluation in 10 Minutes, more
• 2023: Zicklag, Interaction Nets, Combinators, and Calculus
• 2025: Borba, Lazy and Strict Evaluation, Polarized Interaction Net Systems, Lambda Calculus Normalization with Interaction Nets

Videos

• 2023: Taelin, HVM: um Runtime Paralelo [English Subtitles]
• 2024: Higher-Order Company (Taelin, Carman, Abril, and Borba), HVM2: Interaction Combinator Evaluator (FProPer24)
• 2024: Wolfram Institute (Murzin and Wiles) Introduction to Interaction Nets

Research

General

• 1990: Lafont, "Interaction Nets." url
• 1991: Gay, "Interaction Nets." url
• 1994: Asperti and Laneve, "Interaction Systems I." url
• 1996: Asperti and Laneve, "Interaction Systems II." url
• 1997: Lafont, "Interaction Combinators." url
• 2003: Fernández and Mackie, "Operational Equivalence for Interaction Nets." url
• 2006: Ehrhard and Regnier, "Differential Interaction Nets." url
• 2009: Fernández, Mackie, Sato, and Walker, "Recursive Functions with Pattern Matching in Interaction Nets." url
• 2016: Mackie and Sato, "In-place Graph Rewriting with Interaction Nets." url
• 2016: Mackie and Sato, "Parallel Evaluation of Interaction Nets: Case Studies and Experiments." url
• 2016: Gimenez and Moser, "The Complexity of Interaction." url

Implementation

• 2000: Pinto, "Sequential and Concurrent Abstract Machines for Interaction Nets." url
• 2003: Pinto, "Weak Reduction and Garbage Collection in Interaction Nets." url
• 2009: Hassan, Mackie, and Sato, "Compilation of Interaction Nets." url
• 2015: Kahl, "A Simple Parallel Implementation of Interaction Nets in Haskell." url
• 2015: Sato, "Design and Implementation of a Low-Level Language for Interaction Nets." url
• 2020: Accattoli, Lago, and Vanoni, "The Abstract Machinery of Interaction." url
• 2024: Taelin, "HVM2: A Parallel Evaluator For Interaction Combinators." url
• 2025: Huber and Yi, "An Encoding of Interaction Nets in Ocaml." url

Geometry

• 1989: Girard, "Geometry of Interaction 1." url
• 1992: Gonthier, Abadi, and Lévy, "The Geometry of Optimal Lambda Reduction." url
• 1995: Mackie, "The Geometry of Interaction Machine." url
• 2002: Fernández and Mackie, "Call-by-Value λ-Graph Rewriting without Rewriting." url

Syntax

• 1990: Lafont, "Interaction Nets." url
• 1999: Fernández and Mackie, "A Calculus for Interaction Nets." url
• 2005: Mackie, "Towards a Programming Language for Interaction Nets." url

Non-Determinism

• 1999: Alexiev, "Non-Deterministic Interaction Nets." url
• 2002: Fernández and Khalil, "Interaction Nets with McCarthy’s Amb." url
• 2006: Mazza, "Interaction Nets: Semantics and Concurrent Extensions." url

IO

• 2012: Jiresch, "Extending Interaction Nets towards the Real World." url
• 2024: Taelin, "HVM2: A Parallel Evaluator For Interaction Combinators." url

Lambda Calculus

Efficiency

• 1996: Lawall and Mairson, "Optimality and Inefficiency." url
• 1998: Mackie, "YALE: Yet Another Lambda Evaluator Based on Interaction Nets." url
• 2004: Mackie, "Efficient λ-Evaluation with Interaction Nets." url
• 2017: Asperti, "About the Efficient Reduction of Lambda Terms." url

Optimality

• 1980: Lévy, "Optimal Reductions in the Lambda Calculus." url
• 1990: Lamping, "An Algorithm for Optimal Lambda Calculus Reduction." url
• 1992: Gonthier, Abadi, and Lévy, "The Geometry of Optimal Lambda Reduction." url
• 1996: Lawall and Mairson, "Optimality and Inefficiency." url
• 1996: Asperti, Giovannetti, and Naletto, "The Bologna Optimal Higher-Order Machine." url
• 1996: Danos and Regnier, "Reversible, Irreversible and Optimal λ-Machines." url
• 1997: Asperti and Chroboczek, "Safe Operators." url
• 1998: Asperti and Guerrini, "The Optimal Implementation of Functional Programming Languages." url
• 2000: Asperti, Coppola, and Martini, "(Optimal) Duplication Is Not Elementary Recursive." url
• 2003: Coppola and Martini, "Optimizing Optimal Reduction." url
• 2004: van Oostrom, van de Looij, and Zwitserlood, "Lambdascope: Another Optimal Implementation of the Lambda-Calculus." url
• 2005: Guerrini, "Sharing Implementations of Graph Rewriting Systems." url
• 2013: Balabonski, "Weak Optimality, and the Meaning of Sharing." url
• 2014: Pedicini, Pellitta, and Piazza, "Sequential and Parallel Abstract Machines for Optimal Reduction." url
• 2017: Lai, Pedicini, and Piazza, "Abstract Machines, Optimal Reduction, and Streams." url
• 2025: Salvadori, "Δ-Nets." url

Tokens

• 1995: Mackie, "The Geometry of Interaction Machine." url
• 2005: Sinot, "Call-by-Name and Call-by-Value as Token-Passing Interaction Nets." url
• 2006: Sinot, "Token-Passing Nets: Call-by-Need for Free." url
• 2008: Almeida, Pinto, and Vilaça, "Token-Passing Nets for Functional Languages." url
• 2016: Salikhmetov, "Token-Passing Optimal Reduction with Embedded Read-Back." url
• 2018: Muroya and Chica, "Efficient Implementation of Evaluation Strategies via Token-Guided Graph Rewriting." url

Theory

• 1997: Asperti, "P = NP, up to Sharing." url
• 1998: Asperti and Mairson, "Parallel Beta Reduction Is Not Elementary Recursive." url
• 2003: Beckmann, "Exact Bounds For Lengths of Reductions in Typed λ-Calculus." url
• 2004: Baillot and Terui, "A Feasible Algorithm for Typing in Elementary Affine Logic." url
• 2007: Terui, "Light Affine Lambda Calculus and Polynomial Time Strong Normalization." url
• 2013: David, Grygiel, Kozic, Raffalli, Theyssier, and Zaionc, "Asymptotically Almost All λ-Terms Are Strongly Normalizing." url
• 2014: Accattoli and Dal Lago, "Beta Reduction Is Invariant, Indeed." url
• 2022: Lago, "Implicit Computation Complexity in Higher-Order Programming Languages." url

Linear Logic

• 2000: Asperti, Coppola, and Martini, "(Optimal) Duplication Is Not Elementary Recursive." url
• 2000: Mackie, "Interaction Nets for Linear Logic." url
• 2002: Mackie and Pinto, "Encoding Linear Logic with Interaction Combinators." url
• 2019: Aschieri and Genco, "Par Means Parallel." url

Term Rewriting System

• 1998: Fernández and Mackie, "Interaction Nets and Term-Rewriting Systems." url