We provide a categorical procedure to turn graphs corresponding to state spaces of finite state machines into boolean circuits, leveraging on the fact that boolean circuits can be easily turned into zk-SNARKS. Our circuits verify that a given sequence of edges and nodes is indeed a path in the graph they represent. We then generalize to circuits verifying paths in arbitrary graphs. We prove that all of our correspondences are pseudofunctorial, and behave nicely with respect to each other.
This is a paper discussing the foundations of 2-dimensional graphical languages, with a view towards their computer implementation in a 'compiler' for monoidal categories. A minor variant of cubical pasting diagrams, called 'brick diagrams', is introduced, which is used in the Statebox visual programming language.
This paper has been submitted, peer reviewed and accepted to STRING3.
Idris-ct is a library to do formally verified category theory in Idris.
A paper reviewing some of the endeavours in trying to connect Petri nets with free symmetric monoidal categories. A list of requirements such connections should respect if they are meant to be useful for practical/implementation purposes is given, and it is shown how previous approaches do not satisfy them. This depends on trying to make the correspondence functorial in the direction from nets to free symmetric monoidal categories, and it is shown how dropping this immediately honors the given desiderata.
Our team members Fabrizio Genovese and Jelle Herold wrote a paper which uses category theory to extend Petri nets in interesting ways. The paper has been submitted, peer reviewed and accepted to the conference QPL2018.
This document contains the mathematical specification on which much of our implementation endeavors are built. You can read and comment on the Monograph using our annotation tool.
This paper is a collaboration with David Spivak during the 3rd Statebox Summit. It builds on the correspondence between Petri nets and free symmetric strict monoidal categories already investigated in the literature, and present a categorical semantics for Petri nets with guards. This comes in two flavors: deterministic and with side-effects. Using the Grothendieck construction, we show how the guard semantics can be internalized in the net itself.