indexstatic.md
Statebox is building a compositional, diagrammatic protocol language.
We don't believe in a technofix but we do think the tools we are building can address the current environmental, social and (software) engineering problems. Come to the meetup in Amsterdam to see what we are up to!
Dynamic version of this page here
Questions?
camp.md
Category Theory Camp
89 September, Amsterdam
Sorry, the category theory camp is fully booked. :(
We might live stream some lectures!
About the training
The Category Theory Camp is directed at workshop attendees who are not familiar with category theory, and has the purpose of helping them achieve a decent understanding of the topic.
The subsequent workshop will make a pervasive use of category theory, and it is fundamental that people are able to understand each other to work proficiently.
The camp is in particular directed to people with experience in functional programming and type theory, and lectures will be designed accordingly.
Wow.
» List of lectures
» Attendees
campattendees.md
« Camp
List attendees Category Theory Camp
 Fabrizio Genovese  Statebox
 Anton Livaja  Statebox
 Erik Post  Statebox
 Jelle Herold  Statebox
 Alexander Gryzlov  Statebox
 TG  Statebox
 Arian van Putten  Independent Researcher
 Jack Ek  Dapphub
 Denis Erfurt  Dapphub
 Daniel van Dijk  Statebox
 Jonathan Paprocki  Holochain
 Sami Van Ness  Holochain
 Josh Harvey  Lamassu
 Eliana Lorch  Protocol Labs
campprogram.md
« Camp
Day 1  First session
 Purpose of Category Theory
 Definition of Category
 Commutative Diagrams
 Op Categories
 Definition of Functor (co and contravariant)
 Definition of Natural Transformation
 Case Study: Presheaves
 Case Study: Monads and EilenbergMoore Algebras
Day 1  Second Session
 Products
 Terminal Objects
 Pullbacks
 Diagrams
 Cones
 Limits
 Colimits
 Coproducts
 Initial Objects
 Pushouts
 Case Study: Initial FAlgebras
Day 2  First Session
 Parallel Composition: Motivation
 Monoidal Categories
 Monoidal Objects
 Case Study: Monads are Monoids
 Monoidal Functors and their Flavors
 Case study: Products and Coproducts
 Case stufy: Cospan composition
 Free Monoidal Categories
 Grothendieck Construction
 Case Study: From Data Types to Terms
Day 2  Second Session
 Categorical Proofs: Yoneda Lemma
 Case Study: Object classifier
 Cartesian Closed Categories
 Case Study: CurryHowardLambek Isomorphism
 Elements of Enriched Category Theory
workshop.md
Research Workshop
1014 September, Schoorl
Sorry, the research workshop is fully booked. :(
Invited lectures will be live streamed!
Structure
As in the previous workshop held in Zlarin, Croatia, participants will be completely free to organize themselves and cooperate as they wish, and the four topics of research highlighted above should be considered more as guidelines than as constraints.
There will also be some invited talks, that will be livestreamed (links will be provided on this page). Please note that the number of talks will be kept to a bare minimum, seeing that the workshop is mainly researchoriented.
» Attendees
» Topics & Working Groups
 Compositional Models for Petri Nets, 1014 Sept.
 Consensus and Sheaves, 1014 Sept.
 Logic Programming and Hardware, 1014 Sept.
 Open Games and Cryptoeconomics, 1214 Sept.
 Typedefs, 1214 Sept.
» Location
workshopattendees.md
« Workshop
Full list of attendees:
 Erik Post  Statebox
 Alexander Gryzlov  Statebox
 Jelle Herold  Statebox
 Fabrizio Romano Genovese  Statebox
 Anthony Di Franco  Statebox
 Daniel van Dijk  Statebox
 Anton Livaja  Statebox
 Emi Gheorghe  Statebox
 Brendan Fong  MIT
 Neil Ghani  University of Strathclyde
 Pawel Sobocinski  University of Southampton
 Jules Hedges  University of Oxford
 Giovanni Caru  University of Oxford
 Jade Master  University of California, Riverside
 Philip Zahn  Oicos/ University of St. Gallen
 Robin Piedeleu  University of Oxford
 Fabio Gadducci  University of Pisa
 Frederik NorvallForsberg  University of Strathclyde
 Dan Ghica  University of Birmingham
 Daniel Cicala  University of California, Riverside
 Stefano Gogioso  University of Oxford
 Arian van Putten  Independent Researcher
 Francisco Rios  University of Dalhousie
 Blake Pollard  NIST
 Viktor Winschel  Oicos
 Martin Lundfall  Dapphub
 Jack Ek  Dapphub
 Jonathan Paprocki  Holochain
 Denis Erfurt  Dapphub
 Teal Gaure  Statebox
 Josh Harvey  Lamassu
 Eliana Lorch  Protocol Labs
 Yoichi Hirai  Ethereum
 Aron Fischer  Ethereum
workshoplocation.md
« Workshop
Research Workshop Location
The village of Schoorl lies at the foot of the Schoorl dunes: the highest, widest and most diverse dune area of the Dutch coast. Throughout the year, it is a lovely walking and cycling area. Schoorl has 3 climbing dunes. Cycling through the dunes to Schoorl aan Zee (where no cars are allowed) is an experience in itself.
workshoptopics.md
« Workshop
Research Groups
The workshop will address the following research topics, organized in macrogroups:
topiccryptoeconomics.md
« Research Groups
Open Games and Cryptoeconomics, Sept. 12 to Sept. 14
Open games [1] are a new, compositional framework for game theory. In particular, open games allow to infer the existence of Nash equilibria in a game compositionally, that is, considering a game as a composition of subgames.
Intuitively, a Nash equilibrium [2] in a game denotes a strategy from which no player has interest to deviate, because this would translate to a loss of profit (whatever “profit” means depends on the game). A well known example of what Nash equilibria are and how they can sometimes be counterintuitive is given by the famous prisoner’s dilemma.
For a long time it has been thought that games weren’t compositional, since an optimal strategy for a game may cease to be optimal if the game is changed/extended in any way (for instance adding more players). Open games revert this point of view showing how equilibria can indeed be inferred from the subgames the game is composed of.
This field of research is very young and, albeit it is developing incredibly quickly, many problems have still to be solved. For instance, the mathematical machinery developed up to now is still not ready to tackle the issue of repeated games in a satisfactory way.
The Statebox team thinks that open games will become incredibly valuable for (crypto)economic analysis in the future, since their inherent compositionality allows them to scale whereas classical game theory becomes unusable for games beyond a certain level of complexity, which is too low to model any meaningful real scenario. For the same reasons, games could be useful for protocol analysis.
The relationship between Statebox and open games is still not clear, but it is for sure worth investigating. We will mainly focus on the following links:

Open games and cryptoeconomics. Is it possible to describe classical themes in cryptoeconomic using open games? To be more precise, if some cryptoeconomic behavior (such as exchanging currency) can be described in terms of Petri nets, are we able to put open games “on top of them” to obtain an highlevel optimization engine? In this respect, open games could provide the best firing strategies on a net to minimize/maximize some utility function representing something we care about (i.e. transaction fees).

Open games and protocols. Can open games be used to analyze the correctness of consensus protocols? This is heavily linked with the activities of the Consensus group, and it should not be surprising that sheaves of games are already a thing (ask Jules Hedges about this!)! Many consensus protocols – such as [3] – are, indeed, analyzed gametheoretically in contemporary research, but we find the gametheoretic tools employed pretty basic and unsatisfying. Open games could, again, give a wider insight on consensus, allowing us to cast general properties to describe such protocols.

Complexity and implementability: At the moment, open games are really inefficient when it comes to implementations [4]. This is clearly a huge downside, since if compositionality allows for scalability theoretically, this is still not true in practice. We would like to leverage the insights of all the professionals in programming and complexity invited to the workshop to better understand how such a problem could be solved.
Since the links between open games and Statebox are still pretty vague, we decided to start the open games research group two days later with respect to the others. This will allow researchers interested in open games to first gather more information about consensus, Petri nets and the like. In this way, there will be quite a lot of material to throw open games at in the subsequent days!
Useful reads:
[1] Ghani, N., Hedges, J., Winschel, V., & Zahn, P. (2016). Compositional Game Theory. ArXiv:1603.04641 [Cs].
[2] Fundenberg, D., & Tirole, J. (1991). Game Theory. Boston, MA: MIT Press.
[3] Nakamoto, S. (2008). Bitcoin: A PeertoPeer Electronic Cash System, 19.
[4] Papadimitriou, C. H. (1994). On the Complexity of the Parity Argument and Other Inefficient Proofs of Existence. Journal of Computer and System Sciences, 48(3), 498–532.
topichardware.md
« Research Groups
Logic Programming and Hardware, Sept. 10 to Sept. 14
Besides developing a language and runtime software implementation, Statebox is interested in developing a chip capable of executing Statebox protocols. We have particular requirements regarding correctness and security: We want to precisely control and observe what the chip is doing to avoid bugs and security issues.
We will consider the problem both mathematically and empirically: We will bring various devices that can be useful for this, such as a software defined radio device to generate and sample signals, a scope/signal generator, amplifier, multiplexers and target chips for which we have layer masks, such as 6502 and 555. We will moreover bring an FPGA that can be programmed using an entirely freesoftware toolchain called 'Icestorm' [1].
Some of the paths we will explore are:
Compositional Digitial Circuit Synthesis
Programmable logic chips are devices that allow the uploading of a digital circuit made. They achieve this by connecting many small digital circuits, called cells, with a reconfigurable switching bus. A hardware description language such as VHDL [2] is used to design circuits for such a chip. It is a dataflow language, so its programs look like PROPs over stateful digital circuits and binary signals on the wires.
Statebox exhibits a diagrammatic structure similar to what is used in [3]. This suggests two extensions to the Statebox system:
 Replacing Petri nets in a Statebox diagram with digital circuits and constructing a VHDL program which synthesizes into the circuit;
 Translating Petri nets into digital circuits and using the point above to synthesize a chip design.
This is the first step towards a "Statebox chip".
InformationGain Computing Unit
Besides executing Petri nets, we want to do computation (folds). These can be expressed as (compositional) logical queries and executed by an informationgain computation. Anthony Di Franco's approach of logic program evaluation [4] suggests an alternative way to construct a general processing unit: Replacing the cells of a FPGA with something that can perform informationgain specific tasks.
This will be made possile by projects aiming to define a free FPGA [5]. If such a device is realised, it could lead to a new architecture of 'declaratively programmable' chips, acting much more like pure mathematical functions than operationally, like a Turing machine.
During this research workshop we want to start placing this thinking on solid categorical grounds.
Hardware Attestation
How can we attest (cheaply) that our chip does precisely what it should and is in no way tampered with or otherwise broken? And does the chip leak information when it is operated outside of the electrical specifications? [6] (Or is this impossible?)
There is a lot of centralization and trust involved in semiconductors: Chip designs and toolchains are usually proprietary closed systems, with severe security implications [7]. Once built, there is no way of fully verifying the behaviour of a chip without destructively inspecting it, with no guarantees that possible hidden features and bugs will be uncovered in doing so.
We want to design an apparatus that can confirm some fingerprint of the chip by probing it outside of its specified range and measuring the effects of this on various pins. Hopefully we might be able to construct a signature capable of distinguishing topological properties of the die layers/masks.
We can take inspiration from:
 Impulse response techniques, as in listening to the reverberation sound of a gun fired in a space [8];
 The single pixel camera approach developed in [9], considering a single high resolution oscilloscope signal as the pixel and different activations patterns as the light sources;
 Tomographic reconstruction, considering the chip as some sort of nonlinear space and taking an Xray through the pins [10].
Furthermore, we could work on a software based simulation of the physical/electrical aspects based on images of the layer masks, allowing us to explore the problem virtually. Another angle would be to look at power consumption, timing or other sidechannel noise of a simple chip such as the 6502, and see if we can infer 'topological attestations' from this.
Useful reads:
[1] Icestorm Website.
[2] Wikipedia: VHSIC Hardware Description Language.
[3] Ghica, D.R., & Jung, A. (2016). Categorical semantics of digital circuits. In R. Piskac, & M. Talupur (Eds.), Proceedings of the 16th Conference on Formal Methods in ComputerAided Design. Springer Berlin.
[4] Di Franco, A. (2017). InformationGain Computation. ArXiv:1707.01550 [Cs].
[5] Libresilicon Website.
[6] Bernstein, D.J. (2005). Cachetiming attacks on AES.
[7] VaughanNichols, S.J. (2017). MINIX: Intel's hidden inchip operating system.
[8] Wikipedia: Impulse Response.
[9] Candès, E. J., Romberg, J. K., Tao, T. (2006). Stable signal recovery from incomplete and inaccurate measurements. ArXiv:0503066 [Math].
[10] Wikipedia: Tomographic Reconstruction.
topicpetrinets.md
« Research Groups
Compositional Models for Petri Nets
Sept. 10 to Sept. 14
Statebox, as a programming language, is particularly concerned with separating code topology from code meaning. We believe that software design should happen in two stages; Firstly, we define the overall geometry of the software, and only after that we populate this geometry with code snippets that perform particular actions. Note how this reflects the way every programmer works: first one sketches on paper what the code “should do” and then this sketch is used as a guideline to produce the code itself. We are of the opinion that this natural routine should be made formal.
To do this, we decided to use Petri nets as the basic tool to describe software topology, for the following reasons:
 Many systems or processes are adequately modeled using Petri nets.
 Petri nets are inherently visual, making process design and debugging much easier.
 Petri nets admit a categorical formalization (as, for instance, in [1]), with which we can map net transitions into a semantics via functors. This realizes the unification between software topology and software meaning that we wanted to achieve.
Unfortunately, Petri nets are not expressive enough to accomodate our needs. In fact, for every real application, at least composition and recursion are needed.
 Compositionality for Petri nets has been realized categorically in different ways, mainly in terms of transition synchronization [2] and placemerging using the cospan formalism [3].
 Recursion can be realized in terms of nets within nets [4], with the evident disadvantage of losing decidability of important properties such as liveness, boundedness and reachability.
In [5] a model of Petri nets that accomodates both place merging and transition synchronization is proposed, albeit noncategorically. This model has the advantage of losing decidability only for bisimulations (which is good if compared with other solutions), and allows to modularly implement decidable fragments of concurrent calculi such as ACSS [6] and CSP [7]. At the moment, we are evaluating if such formalism is enough to model everything we need for protocol design. In any case, a categorification of [5] would be a wonderful starting point for the unification of the different categorical formalisms presented so far.
In this working group, we are then concerned with three main problems:
 Categorification of [5];
 Assessing the real potential of [5] in terms of expressivity in protocol design;
 Assessing the challenges in implementing petrinet based protocol design tools, and finding solutions.
Useful reads
[1] Sassone, V. (1995). On the Category of Petri Net Computations. In P. D. Mosses, M. Nielsen, & M. I. Schwartzbach (Eds.), TAPSOFT ’95: Theory and Practice of Software Development (Vol. 915, pp. 334348). Berlin, Heidelberg: Springer Berlin Heidelberg.
[2] Bruni, R., Melgratti, H., Montanari, U., & Sobocinski, P. (2013). Connector Algebras for C/E and P/T Nets’ Interactions. Logical Methods in Computer Science, 9(3).
[3] Fong, B. (2015). Decorated Cospans. Theory and Applications of Categories, 30(33).
[4] KöhlerBußmeier, M. (2014). A Survey of Decidability Results for Elementary Object Systems. Fundamenta Informaticae, (1), 99123. https://doi.org/10.3233/FI2014983
[5] Baldan, P., Bonchi, F., & Gadducci, F. (2009). Encoding Asynchronous Interactions Using Open Petri Nets. In M. Bravetti & G. Zavattaro (Eds.), CONCUR 2009  Concurrency Theory (Vol. 5710, pp. 99114). Berlin, Heidelberg: Springer Berlin Heidelberg.
[6] Amadio, R. M., Castellani, I., & Sangiorgi, D. (1996). On Bisimulations for the Asynchronous πCalculus. In U. Montanari & V. Sassone (Eds.), CONCUR ’96: Concurrency Theory (Vol. 1119, pp. 147162). Berlin, Heidelberg: Springer Berlin Heidelberg.
[7] Hoare, C. A. R. (1985). Communicating Sequential Processes. Englewood Cliffs, US: PrenticeHall.
topicsheaves.md
« Research Groups
Consensus and Sheaves, 1014 Sept.
The study of consensus protocols for decentralized systems has become a very active topic of research in the last decade. The original PoWbased consensus protocol by Nakamoto [1] has evolved into different propositions to overcome its downsides (such as energy consumption and lack of scalability). This resulted in PoSbased consensus, such as [2], and DAGbased consensus, as in [3] and [4]. These two approaches are quite different:

PoSbased consensus represents data in the form of a linearly ordered chain of blocks, where adding inconsistent information causes the chain to fork. Consensus here means having a deterministic and reliable procedure to always establish which chain is the “true” one, i.e. a procedure to decide which branch is the one to be used.

In DAGbased consensus, instead, information is organized into a directed acyclic graph of blocks. Blocks that represent contradictory information are still allowed to live on it (inconsistent information doesn’t cause forking), and consensus is reached by means of a “voting procedure” where the value of each block is calculated in terms of graphtheoretic properties. If the same information (i.e. “how much money do I own?”) is reported by different blocks inconsistently, the voting procedure deterministically allows to decide which block is the one to use.
The tools used to study consensus up to now have been quite rudimentary from the theoretical point of view, and consist mainly of probabilistic arguments, such as random walks, and basic game theory.
On the other hand, sheaf theory [5] has been successfully applied to data representation and analysis [6] thanks to the inherent capacity that sheaves have in representing conflicting information. At Statebox, we are convinced that the underlying theory of consensus protocols can be neatly categorified using sheaves, and we want to bootstrap this research endeavor at the workshop. In particular, in the DAGbased approach it is clear that the properties of the consensus protocol allow for information to be locally consistent but globally inconsistent, a perspective that has striking similarities with the one adopted in sheaftheoretic contextuality [7].
Our gut feeling is that a generic consensus protocol could be characterized sheaftheoretically as follows:
 The information, that may contain inconsistent statements, is organized as a presheaf;
 A consensus protocol is a way to lift this presheaf into a sheaf, where some properties have to hold.
This being true, different consensus protocols would just be different presheaves/sheaves used to organize the same information. Such highlevel perspective would allow for a contextualitybased study of consensus, with all the inherent benefits of having a huge categorical arsenal to at our service.
At the moment, this is nothing more than an idea, and we will need to put in some solid brain work to turn it into something more.
At the workshop, the goals for this group will be:
 Review [1], [2], [3] and [4] from a sheaftheoretic perspective;
 Propose a generalized consensus theory based on sheaves;
 Assess which desirable properties for consensus algorythms can be captured sheaftheoretically, and if this is enough to make further endeavors worth;
 Assess the feasibility of the sheaftheoretic method implementationwise, that is: Is there an efficient way to turn a sheafbased model into code? What are the difficulties we have to overcome to reach this goal?
Useful reads:
[1] Nakamoto, S. (2008). Bitcoin: A PeertoPeer Electronic Cash System, 19.
[2] Buterin, V., & Griffith, V. (2017). Casper the Friendly Finality Gadget. ArXiv:1710.09437 [Cs].
[3] Sompolinsky, Y., Lewenberg, Y., & Zohar, A. SPECTRE. Serialization of Proofofwork Events: Confirming Transactions via Recursive Elections (pp. 166).
[4] Sompolinsky, Y., & Zohar, A. PHANTOM: A Scalable BlockDAG protocol (pp. 126).
[5] Mac Lane, S., & Moerdijk, I. (1992). Sheaves in Geometry and Logic, a First Introduction to Topos Theory. (S. Axler, F. W. Gehring, & K. A. Ribet, Eds.) (Vol. 13). New York: Springer.
[6] Robinson, M. (2014). Topological Signal Processing. Berlin, Heidelberg: Springer Berlin Heidelberg.
[7] Abramsky, S., & Brandenburger, A. (2011). The SheafTheoretic Structure Of NonLocality and Contextuality. New Journal of Physics, 13(11), 113036.
topictypedefs.md
« Research Groups
Typedefs
Turning data (bits) into information (typed terms) and back again is a very basic operation that occurs in most softwares.
In general, the need to translate typed terms back and forth to bitstrings – or to (de)serialize them, as it is usually said – comes from the need to read and write them from and to a storage medium or to communicate such terms over some sort of message channel.
Thus, this is often combined with some form of Remote Produre Call specification ability.
Parsers are also a common source of security bugs, so people often use tools to generate code from a specification and avoid having to implement and audit it yourself.
Current approaches for this include
 XDR
 XML /
 JSON / JSONSchema
 Google’s protocol buffers
 Facebook’s Thrift, etc.
 Apache Avro
 Capnproto
plate
 Cheerios, verified (de)serialization lib, a part of the http://distributedcomponents.net/ project
 Kaitai
 Universal Binary Format
 and many more, see for instance
dloss/binaryparsing
 or check wikipedia: Comparison of data serialization formats
Most of the standards mentioned above, though, are not categorically framed, and this results in the paradoxical situation in which a serialization method may does not fit well to typed terms in some underlying type theory.
Clearly, this lack of theoretical ground becomes problematic in applications that rely heavily on type theory, such as functional programming and the language Statebox is developing.
We are set on fixing this: Typedefs is a categoricalbased serialization protocol for types. We need it to be as much universal as possible, to ensure seamless communication between a general spectrum of different type theories and programming. For this reason, the core of typedefs is pretty simple, and focuses on types obtained from the constructors 0, 1, sums and products between them, and a controlled form of recursion.
In technical terms, we started describing Typedefs in terms of initial FAlgebras [1], which results in the ability to formalize only finite data structures. Our FAlgebras are defined for endofunctors on the category of sets formed only by finite products and coproducts of initial and terminal objects. Incredibly, this is enough to express common data structures such as booleans, natural numbers, lists, trees and so on. The actual existence of such inital algebras and their computation relies heavily on Adamek’s [2] and Lambek’s [3] theorems, as any type theorist would legitimately guess. What is left to do is internalizing the naming conventions and serialization procedure itself to ensure ultimate consistency, and to implement it. A prototypical implementation of Typedefs in Idris [4] is already being worked out.
The goal of this research group will be:
 Work out the categorical formalization of serialization, and studying how this relates to hashing algorithms.
 Focus on the current Idris implementation and its efficiency.
 Starting to implement Typedefs in other languages.
Useful Reads:
[1] Pierce, B. C. (1991). Basic Category Theory for Computer Scientists. Cambridge, Massachusetts: The MIT Press.
[2] Adámek, J. (1974). Free Algebras and Automata Realizations in the Language of Categories. Commentationes Mathematicae Universitatis Carolinae, 15(4), 589602.
[3] Lambek, J. (1968). A Fixpoint Theorem for Complete Categories. Mathematische Zeitschrift, 103(2), 151161.
[4] Brady, E. (2013). Idris, a GeneralPurpose Dependently Typed Programming Language: Design and Implementation. Journal of Functional Programming, 23(05), 552593.
[5] Geest, Swierstra Generic Packet Descriptions: Verified Parsing and Pretty Printing of LowLevel Data
[6] Suriyakarn, PitClaudel, Delaware, Chlipala, NARCISSUS: Deriving CorrectByConstruction Decoders and Encoders from Binary Formats
[7] Binary parsing, based on the stuff in Power of Pi gist
meetup.md
The Very Blockchain Meetup — 15 September, Amsterdam
The event is featuring speakers from academia, the hacker culture and the business world, marking the end of the Second Statebox Summit. You can expect good company, a series of compelling talks, music and food. This is an opportunity for anyone to meet team members, advisors, partners and friends of Statebox.
Some topics addressed in the talks are related to:
 functional programming
 diagrammatic reasoning
 category theory
 cryptoeconomics
 the impact of the blockchain technology on society
Preliminary list of speakers/talks:
 Josh Harvey (Lamassu: Bitcoin ATM)  Cashing in on Statebox
 Bob Coecke (Quantum Group, Oxford University)  What are Diagrammatic Languages
 Florian Glatz (Statebox, Bundesblock, Blockchain Embassy)  Law was Code before Code was Law
 Holochain  Ethical Computing and Natural Systems
 Guts Tickets
 Viktor Winschel (Oicos)  Finally: a Money Theory and a Bank for Central Banks
 Amin Rafiee  Gamification of Life
The full list of speakers, program and tickets will be available soon.
Meanwhile, follow us on twitter, meetup or telegram.
Thanks to Holochain and Guts Tickets for sponsoring the event!