Paper 2022/1211

Arithmetization of Functional Program Execution via Interaction Nets in Halo 2

Anthony Hart, Orbis Labs

We sketch a method for creating a zero-knowledge proof of knowledge for the correct execution of a program within a model of higher-order, recursive, purely functional programming by leveraging Halo 2. To our knowledge, this is the first ZKP for general purpose computation based on purely functional computation. This is an attractive alternative to using a von Neumann architecture based zero-knowledge virtual machine for verified computing of functional programs, as compilation will be more direct, making it more easily verifiable and potentially more efficient. Interaction nets are a natural setting for recursive, higher-order functional programming where all computation steps are linear and local. Interaction nets are graphs and traces for such programs are hyper-graphs. Correctness of a trace is a simple syntactic check over the structure of the trace represented as a hyper-graph. We reformulate this syntactic check as a Halo 2 circuit which is universal over all traces.

Available format(s)
Publication info
Functional Programming Halo 2 Interaction Nets Combinators Lambda Calculus String Diagrams
Contact author(s)
team @ orbislabs com
2022-09-14: approved
2022-09-13: received
See all versions
Short URL
Creative Commons Attribution


      author = {Anthony Hart},
      title = {Arithmetization of Functional Program Execution via Interaction Nets in Halo 2},
      howpublished = {Cryptology ePrint Archive, Paper 2022/1211},
      year = {2022},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.