Overview of the Statebox summit in Zlarin, Croatia, 1-7 Nov. 2017
Our summit will be organized in distinct phases:
Phase 0 (Oct 30 - Oct 31)
This is when we will set up the house (routers, projectors, whiteboards, …) and people arriving early will be able to get to know each other.
Phase I (Nov. 1 - Nov. 2) - Program
At the moment the Statebox Team is contacting some of the people invited and filling up the remaining speaking slots. The program is not yet finalized. A final version will be updated in the next few days.
To take place on 1st and 2nd of November, it will consist of a series of scientific talks where the researchers invited will have the opportunity to talk about aspects from their area of expertise, which are also relevant to the Statebox project. The talks will be interactive. The goal here is to not simply present one’s own work, but to enable people to manipulate it and use it in the next days (at least to some extent). The duration of each talk will be agreed with the relevant speakers. A big part of the talk time slot will be dedicated to questions/interaction with the crowd.
At the end of each day, a couple of special talks will be given. Those will be about the current blockchain environment, the hacker culture and how to make business in the cryptocurrency community.
Phase II (Nov. 3 - Nov. 6)
It will take place between November 3 to November 6. People will have the opportunity to freely organize themselves in microclusters and employ their skills to solve relevant problems.
The goal of phase II is to start putting in place solid mathematical foundations to formalize the vision underlying Statebox. This is when the fun happens. The Zlarin house(s) will transform into open labs, where people will be able to chat and cooperate as they wish, and put their skills to good use. There will not be any time limits/slots of sorts: You will be free to work/think about the problems hereby listed while taking a walk in the forest, scribbling on a whiteboard or while fishing on the seashore. Also the fun vs. time ratio is up to you: If you are a workaholic you are free to work 48 hours straight. The same applies if you need to take a nap every 15 minutes. We believe that such an approach is more respectful of everyone’s personal rhythm, hence we are actively advocating for such a policy: The model we have in mind is about letting people self-organize in mini-clusters of 3-4 people each, according to their interests. These mini-clusters are flexible, meaning that everyone is able to hop around from one to the other, according to their will, for as long as he/she wishes.
At the end of each day, a brief review of the things we figured out will be given. Everything will be documented with pictures/posts on a dedicated blog.
The main problems to be solved are:
- Relate string diagrams with Petri nets: Statebox will in fact use a mix of the two. A strong mathematical formalism relating them in a consistent way is needed to implement strongly desiderated features, such as code correctness and formal verification. This will essentially be the category theory people’s lunapark.
- Structure a well founded business model using math: Before going public and launching Statebox on the blockchain, we want to work out the best way to do this using results in mathematical economics. In particular, we want to design the best auction mechanism for Statebox initial sale and further discuss the revenue model we already set in place for it. People interested in money theory will have the opportunity to put their skills to good use to solve this problem.
- Study the implementability of our model in Idris: Once point 1 is clarified, we will have to start thinking about possible coding strategies to actually implement it. This is where functional programming people will probably have the most fun.
- Figure out formal verification for string diagrams: String diagrams represent pieces of code in Statebox. We clearly want to have a way to optimize this code according to relevant parameters: This is another problem to which we will have to give some thought.
- Formalize the interaction between open games and Petri nets: Can open games be used to optimize the firing patterns in a Petri net, or to verify their overall consistency? We think the answer is yes, but then again the relevant maths has to be put in place.
Phase III (Nov. 7 - Nov. 8)
Here we will review everything we did, we will set new deadlines/milestones and we will figure out, according to contributions/time to dedicate to the project, who to take on board as a team member or as an advisor.
On November 9, finally, we will “reset” the house and leave it for good.
If you want to do some homework before showing up, here is a reading list of papers that you may wish to skim through. Moreover, we have a Mendeley group where these paper are shared. If you use Mendeley, we strongly suggest you request access to the group clicking on the following link (feel free to add any relevant paper to the Mendeley repo):
Mac Lane, S. Categories for the working mathematician, Springer, New York 1978
Borceux, F. Handbook of Categorical Algebra, Volumes 1,2,3, Cambridge University Press, Cambridge 1994
Selinger, P. A Survey of Graphical Languages for Monoidal Categories, In Bob Coecke (ed.). New Structures for Physics. Lecture Notes in Physics. Springer Berlin Heidelberg, 2010. pp. 289-355. arXiv:0908.3347.
Coecke, B. and Kissinger, A. Picturing Quantum Processes. A First Course in Quantum Theory and Diagrammatic Reasoning, Cambridge University Press, Cambridge, 2017.
Sobocinksi, P. Representations of Petri nets interactions, 6269 LNCS, 2010.
Baez, J. and Pollard, B. A compositional framework for reaction networks, Reviews in Mathematical Physics 29 (2017), 1750028.
Baez, J. Quantum techniques for reaction networks, to appear in Natural Computing.
Works by: Jose Meseguer, Ugo Montanari, Vladimiro Sassone
Hedges, J. Towards compositional game theory, Queen Mary University of London (PhD Thesis).
Functional Programming / Formal Verification
Brady, E. Type-driven Development with Idris, Manning Publications, 2017.
Di Franco, A. Information-gain Computation, arXiv: 1707.01550.
Subscribe to our mailinglist to get (low volume) news