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.

- Mapping Finite State Machines to zk-SNARKS Using Category Theory 1909.02893

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.

- Foundations of Brick Diagrams 1908.10660

Idris-ct is a library to do formally verified category theory in Idris.

We also published a paper about this, which has been submitted, peer reviewed and accepted to the conference ACT2019. A conference talk can be found here.

- Idris-ct: A Library to do Category Theory in Idris 1912.06191.

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.

- Computational Petri Nets: Adjunctions Considered Harmful 1904.12974

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.

You can find the paper here, along with presentation talks here (short) and here (long).

- Executions in (Semi-)Integer Petri Nets are Compact Closed Categories 1805.05988

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.

- The Mathematical Specification of the Statebox Language 1906.07629

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.

- A Categorical Semantics for Guarded Petri Nets 2002.02762