index-static.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

8-9 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


camp-attendees.md

« Camp

List attendees Category Theory Camp

  1. Fabrizio Genovese - Statebox
  2. Anton Livaja - Statebox
  3. Erik Post - Statebox
  4. Jelle Herold - Statebox
  5. Alexander Gryzlov - Statebox
  6. TG - Statebox
  7. Arian van Putten - Independent Researcher
  8. Jack Ek - Dapphub
  9. Denis Erfurt - Dapphub
  10. Daniel van Dijk - Statebox
  11. Jonathan Paprocki - Holochain
  12. Sami Van Ness - Holochain
  13. Josh Harvey - Lamassu
  14. Eliana Lorch - Protocol Labs

camp-program.md

« Camp

Day 1 - First session

Day 1 - Second Session

Day 2 - First Session

Day 2 - Second Session

workshop.md

Research Workshop

10-14 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 research-oriented.

» Attendees

» Topics & Working Groups

» Location


workshop-attendees.md

« Workshop

Full list of attendees:

  1. Erik Post - Statebox
  2. Alexander Gryzlov - Statebox
  3. Jelle Herold - Statebox
  4. Fabrizio Romano Genovese - Statebox
  5. Anthony Di Franco - Statebox
  6. Daniel van Dijk - Statebox
  7. Anton Livaja - Statebox
  8. Emi Gheorghe - Statebox
  9. Brendan Fong - MIT
  10. Neil Ghani - University of Strathclyde
  11. Pawel Sobocinski - University of Southampton
  12. Jules Hedges - University of Oxford
  13. Giovanni Caru - University of Oxford
  14. Jade Master - University of California, Riverside
  15. Philip Zahn - Oicos/ University of St. Gallen
  16. Robin Piedeleu - University of Oxford
  17. Fabio Gadducci - University of Pisa
  18. Frederik Norvall-Forsberg - University of Strathclyde
  19. Dan Ghica - University of Birmingham
  20. Daniel Cicala - University of California, Riverside
  21. Stefano Gogioso - University of Oxford
  22. Arian van Putten - Independent Researcher
  23. Francisco Rios - University of Dalhousie
  24. Blake Pollard - NIST
  25. Viktor Winschel - Oicos
  26. Martin Lundfall - Dapphub
  27. Jack Ek - Dapphub
  28. Jonathan Paprocki - Holochain
  29. Denis Erfurt - Dapphub
  30. Teal Gaure - Statebox
  31. Josh Harvey - Lamassu
  32. Eliana Lorch - Protocol Labs
  33. Yoichi Hirai - Ethereum
  34. Aron Fischer - Ethereum

workshop-location.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.

workshop-topics.md

« Workshop

Research Groups

The workshop will address the following research topics, organized in macro-groups:

» Compositional Models for Petri Nets, 10-14 Sept.

» Consensus and Sheaves, Sept. 10 to Sept. 14

» Logic Programming and Hardware, 10-14 Sept.

» Open Games and Cryptoeconomics, 12-14 Sept.

» Typedefs, 12-14 Sept.

topic-cryptoeconomics.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 sub-games.

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 sub-games 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:

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 Peer-to-Peer Electronic Cash System, 1-9.

[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.

topic-hardware.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 free-software 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:

This is the first step towards a "Statebox chip".

Information-Gain Computing Unit

Besides executing Petri nets, we want to do computation (folds). These can be expressed as (compositional) logical queries and executed by an information-gain 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 information-gain 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:

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 side-channel 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 Computer-Aided Design. Springer Berlin.

[4] Di Franco, A. (2017). Information-Gain Computation. ArXiv:1707.01550 [Cs].

[5] Libresilicon Website.

[6] Bernstein, D.J. (2005). Cache-timing attacks on AES.

[7] Vaughan-Nichols, S.J. (2017). MINIX: Intel's hidden in-chip 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.

topic-petrinets.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:

Unfortunately, Petri nets are not expressive enough to accomodate our needs. In fact, for every real application, at least composition and recursion are needed.

In [5] a model of Petri nets that accomodates both place merging and transition synchronization is proposed, albeit non-categorically. 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:

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öhler-Bußmeier, M. (2014). A Survey of Decidability Results for Elementary Object Systems. Fundamenta Informaticae, (1), 99-123. https://doi.org/10.3233/FI-2014-983

[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: Prentice-Hall.

topic-sheaves.md

« Research Groups

Consensus and Sheaves, 10-14 Sept.

The study of consensus protocols for decentralized systems has become a very active topic of research in the last decade. The original PoW-based 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 PoS-based consensus, such as [2], and DAG-based consensus, as in [3] and [4]. These two approaches are quite different:

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 DAG-based 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 sheaf-theoretic contextuality [7].

Our gut feeling is that a generic consensus protocol could be characterized sheaf-theoretically as follows:

This being true, different consensus protocols would just be different presheaves/sheaves used to organize the same information. Such high-level perspective would allow for a contextuality-based 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:

Useful reads:

[1] Nakamoto, S. (2008). Bitcoin: A Peer-to-Peer Electronic Cash System, 1-9.

[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 Proof-of-work Events: Confirming Transactions via Recursive Elections (pp. 1-66).

[4] Sompolinsky, Y., & Zohar, A. PHANTOM: A Scalable BlockDAG protocol (pp. 1-26).

[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 Sheaf-Theoretic Structure Of Non-Locality and Contextuality. New Journal of Physics, 13(11), 113036.

topic-typedefs.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

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 categorical-based 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 F-Algebras [1], which results in the ability to formalize only finite data structures. Our F-Algebras 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:

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 General-Purpose 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 Low-Level Data

[6] Suriyakarn, Pit-Claudel, Delaware, Chlipala, NARCISSUS: Deriving Correct-By-Construction 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:

Preliminary list of speakers/talks:

The location is tq.co.

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!