Martin Coll

I'm happy to share my first paper ever. Thanks to my amazing collaborators for this opportunity🎉

@apoth3osis_io @SpeakezTech @JustDeezGuy Sounds the same. From the Lean perspective, MLIR is a monolith accessible only through the formal dialect IR. On the MLIR side, you lower the formal IR dialect to the target architecture. The other end is targeting the architecture without an intermediate dialect.

If I were building this for public usage I think that would be sound advice. As I understand our current setup, the separation is already there: the Lean ICC formalization IS the formal semantics, verified independently. The Inet dialect would be the compilation target, not the verification layer. Lean proves the reductions correct, Inet MLIR handles lowering to hardware. Two separate concerns, two separate systems, one correspondence theorem connecting them. Does that match what you are describing?

@apoth3osis_io @SpeakezTech @JustDeezGuy I would keep a separate verification dialect, follow existing work. In this case the Inet dialect *is* the formal semantics, and lowering to GPU, CPU ot anything else is user choice. dl.acm.org/doi/10.1145/37…

Yes, HVM4 is our runtime. The current pipeline is Lean ICC terms compiled through a 25-phase SKY combinator pipeline down to interaction nets that execute on GPU via HVM4. The piece I have been wanting to build is exactly what you are describing: the Inet dialect at compile time to replace the hand-written lowering, with HVM4 still handling runtime reduction on GPU. So the compile-time graph rewriting in your dialect would give me verified lowering from Lean to interaction nets, and HVM4 continues to handle the actual parallel reduction. The runtime side you mention as not done yet is interesting. Is the idea that the Inet dialect would eventually have its own runtime path independent of HVM? Or is the intent more that the dialect provides the MLIR-level representation and then backends like HVM handle execution?

@apoth3osis_io @SpeakezTech @JustDeezGuy That's great to know 😁 The graph rewriting should be implemented both at compile time (Inet dialect) and at runtime (not done yet) in order to implement runtime behavior. Are you using HVM as runtime?

🙋 There is only one of me so I am not sure that qualifies as community interest but here I am. Last 2+ years spent following the Kenneth Stanley credo for research, in my own way of course as I do still put in 10-12 hours 6-7 days a week. Actively taking all that R&D and applying it as we speak. The ball is firmly in your court :)

@apoth3osis_io @SpeakezTech @JustDeezGuy There's lots of us :) The dialect is in the same state as I presented in the design meeting, and I would be happy to go back to it for a real world use case. Further development is awaiting community interest. github.com/colltoaction/m… discourse.llvm.org/t/open-mlir-me…

@colltoaction Thanks, and appreciate the kind words on the site. Believe it or not I suffer from Aphantasia to a degree; always drives my wife nuts as somehow my designs come out pretty good, quickly while she belabors the same work :) Your Inet dialect looks like the piece I have been missing. I have Lafont's three combinators formalized in Lean 4 with verified reduction semantics and a GPU execution path through HVM4. The problem I keep hitting is getting from verified ICC terms to a real compilation target without hand-writing CUDA kernels. To get around this I have been waist deep developing LeanCP, a Lean-native C verifier. I can currently do syntactically and semantically verified Lean to C with an independent C verifier and I am trying to extend coverage to all C functions. It works but expanding it is a nightmare. Your dialect would let me sidestep that entire C layer for interaction net computation and go straight from verified Lean ICC terms to MLIR. What I am going to try to do is build an export path from Lean ICC terms to Inet MLIR so the reductions I prove correct can compile to hardware through MLIR instead of through handwritten GPU code. If you could point me at the current state of the dialect, whether the TableGen rewrite patterns are stable, and any gotchas, that could save me weeks. Happy to further discuss and share more about what I have on the Lean side of course. Three groups independently formalizing the same three combinators from different angles seems like something worth devoting proper attention to.

@apoth3osis_io @SpeakezTech @JustDeezGuy 👋🏻 I'd be happy to help. @apoth3osis_io pretty cool website and engineering worldview 😉.

Absolutely. @colltoaction's Inet dialect is the exact interface point between our verified reduction semantics and your compilation pipeline. Would welcome that connection. Open to any and all help here. The work is progressing, we have been using SKY combinators as a bridge to interaction nets but it has been slow going on the GPU kernel side, which is exactly what the Inet MLIR path would resolve. Honestly there are very few people who seem to realize the size of what is at stake in this space.

I've been implementing Mytilus support in mini-swe-agent and replicating SWE-bench. Models understand the production rules and write shell command pipelines using YAML as effectively as Bash scripts. mini-swe-agent.com/latest/ arxiv.org/abs/2310.06770

I'm working on a C compiler where the intermediate representation is based on the single-instruction Run language by Dusko Pavlovic. Most features are grammar transformations defined in Lex and Yacc files, and C for the remaining implementation. github.com/titi-org/titi-…

New hypergraph library dropped nature.com/articles/s4159…

more proof that trees are bad for syntax, and hypergraphs are better

A little rest from higher-order networks: I'm also doing some compiler work youtu.be/XKY4LLBwmmg

Save the date! June 2 at @NetSciConf I will be presenting the Hypergraph Interchange Format. netsci.nascol.net/abstracts/hif.…

I'm actively looking for cofounders to build general-purpose, massively parallel computer architectures on the basis of Interaction Nets. If you're talented and have some experience in hardware design, compiler engineering or models of computation feel free to DM me

@nilscmr YAML fan

Abandon curly braces and embrace significant indentation

Come find me tomorrow for a demo of Interaction Nets in MLIR discourse.llvm.org/t/open-mlir-me…

Curso Introducción a la Computación Cuántica, edición 2025, año internacional de la ciencia y la tecnología cuánticas. academia.sadio.org.ar/introduccion-a…

"Tensor Species" by @andrewdudzik 🧮🐒 A great talk at the @ToposInstitute Colloquium, overviewing our team's category-theoretic vision for understanding AI systems through CS primitives... ...casually algebrafying einsums and softmax in the process 🐈 youtube.com/live/xBI03pvUn…

📢If you’re interested in Temporal Networks, consider joining the TENET satellite @NetSciConf in Maastricht!🔎We accept one-page abstracts concerning all aspects of temporal network theory, as well as real-world applications. 📅Deadline: February 7 info 👉🏻 tinyurl.com/27ntstep

Another year, another edition!💥 Join #TopoNets25 at @NetSciConf in Maastricht and send us your work on higher-order networks: structure, dynamics, methods, inference, software, topology, #TDA, etc. 📅 Submit by Feb 7th to give a contributed talk: sites.google.com/view/toponets2…

✅ Adjoint School application