Research
Statebox Research is focused on finding universal structures (ie. categorification) of computational aspects. Our research topics cover:
- categorical & diagrammatic languages
- compositional game theory
- epistemic / cryptographic / topological structures
- type theory for category theory
Monograph
The Mathematical Specification of the Statebox Language
This document contains the mathematical specification on which much of our implementation endeavors are built. Put simply, Statebox can be seen as a clever way to tie together different theoretical structures to maximize their benefits and limit their downsides.
More...
This document contains the mathematical specification on which much of our implementation endeavors are built. Put simply, Statebox can be seen as a clever way to tie together different theoretical structures to maximize their benefits and limit their downsides.
More...
Publications
A Categorical Semantics for Hierarchical Petri Nets
We define hierarchical nets, which are Petri nets that can recursively call other Petri nets when a transition is fired. This can be expecially useful to model interacting smart contracts in a decentralized environment. We define everything using category theory, so that it natively fits our current framework as an extension.
More...
We define hierarchical nets, which are Petri nets that can recursively call other Petri nets when a transition is fired. This can be expecially useful to model interacting smart contracts in a decentralized environment. We define everything using category theory, so that it natively fits our current framework as an extension.
More...
A Categorical Semantics for Bounded Petri Nets
There is a well known way in traditional Petri net literature to turn a net into a bounded one, that is, a net where places can only host a finite, pre-determined number of tokens. We prove that this construction is nicely formalized in categorical terms, and that bounded nets can be considered categorical "extensions" of traditional nets.
More...
There is a well known way in traditional Petri net literature to turn a net into a bounded one, that is, a net where places can only host a finite, pre-determined number of tokens. We prove that this construction is nicely formalized in categorical terms, and that bounded nets can be considered categorical "extensions" of traditional nets.
More...
Nets with Mana: A Framework for Chemical Reaction Modelling
We use category theory to formalize the idea of Petri nets endowed with "mana", that is, parameters representing the fact that a transition can only be used a finite number of times. Mana can also eventually be regenerated. We wrote this paper with self-sustaining biochemical reaction in mind, but it can be used also to model message-passing in computer environments. The mana construction fits in the categorical extensions of Petri nets framework that we invented.
More...
We use category theory to formalize the idea of Petri nets endowed with "mana", that is, parameters representing the fact that a transition can only be used a finite number of times. Mana can also eventually be regenerated. We wrote this paper with self-sustaining biochemical reaction in mind, but it can be used also to model message-passing in computer environments. The mana construction fits in the categorical extensions of Petri nets framework that we invented.
More...
Categories of Nets
Traditionally, many different flavors of Petri nets have been defined. In the last thirty years, these structures have been linked to various flavors of monoidal categories, a pervasive structure in category theory, in many ways. In this paper we give a comprehensive overview of these correspondences that one can find in the literature. We moreover show how Sigma-nets, a relatively unknown flavor of Petri nets, are central to presenting all of these correspondences in a neat and consistent way.
More...
Traditionally, many different flavors of Petri nets have been defined. In the last thirty years, these structures have been linked to various flavors of monoidal categories, a pervasive structure in category theory, in many ways. In this paper we give a comprehensive overview of these correspondences that one can find in the literature. We moreover show how Sigma-nets, a relatively unknown flavor of Petri nets, are central to presenting all of these correspondences in a neat and consistent way.
More...
A Categorical Semantics for Guarded Petri Nets
Guarded Petri nets, also known as coloured Petri nets, are an extenson of Petri nets where tokens carry properties and transitions rely on these properties to process them. They have been known for decades, but in this paper we prove that they fit nicely in the framework of Applied Category Theory: Indeed, they can be obtained from standard Petri nets by applying a categorical tool called Grothendieck construction.
More...
Guarded Petri nets, also known as coloured Petri nets, are an extenson of Petri nets where tokens carry properties and transitions rely on these properties to process them. They have been known for decades, but in this paper we prove that they fit nicely in the framework of Applied Category Theory: Indeed, they can be obtained from standard Petri nets by applying a categorical tool called Grothendieck construction.
More...
Idris-CT
In this paper we present an Idris library called idris-ct. Its purpose is being able to do category theory in a formally verified environment, also by keeping things practical as much as possible. In particular, we explore in detail the specifics of our library, and explain the design choices we made.
More...
In this paper we present an Idris library called idris-ct. Its purpose is being able to do category theory in a formally verified environment, also by keeping things practical as much as possible. In particular, we explore in detail the specifics of our library, and explain the design choices we made.
More...
Mapping Finite State Machines to zk-SNARKS Using Category Theory
It is well known that Boolean circuits can be turned into zero knowledge proofs such as ZK-SNARKs using already available software libraries. Here, we provide a categorical procedure to turn graphs corresponding to state spaces of finite state machines into Boolean circuits. Piping our procedure with the above-mentioned software libraries results in a streamlined workflow to turn a finite state machine into a ZK-SNARK.
More...
It is well known that Boolean circuits can be turned into zero knowledge proofs such as ZK-SNARKs using already available software libraries. Here, we provide a categorical procedure to turn graphs corresponding to state spaces of finite state machines into Boolean circuits. Piping our procedure with the above-mentioned software libraries results in a streamlined workflow to turn a finite state machine into a ZK-SNARK.
More...
Computational Petri Nets: Adjunctions Considered Harmful
Historically, people tried to describe the relationship between Petri nets and monoidal categories in many different ways. In this paper we review such endeavours, and point out how many of them fall short of satisfying some necessary requirements for a viable implementation. We then propose an alternative way of linking Petri nets with monoidal categories which in our opinion serves implementation purposes better.
More...
Historically, people tried to describe the relationship between Petri nets and monoidal categories in many different ways. In this paper we review such endeavours, and point out how many of them fall short of satisfying some necessary requirements for a viable implementation. We then propose an alternative way of linking Petri nets with monoidal categories which in our opinion serves implementation purposes better.
More...
Executions in (Semi-)Integer Petri Nets are Compact Closed Categories
We define an extension of Petri nets where tokens are coupled with anti-tokens. If a token can be seen as a resource of some kind, an anti-token represents the lack of a resource. Using category theory, we prove how executions of these nets correspond to Compact Closed Categories, that are relevant structures in Categorical Quantum Mechanics.
More...
We define an extension of Petri nets where tokens are coupled with anti-tokens. If a token can be seen as a resource of some kind, an anti-token represents the lack of a resource. Using category theory, we prove how executions of these nets correspond to Compact Closed Categories, that are relevant structures in Categorical Quantum Mechanics.
More...