Newsletter April
Our newsletter is 1 year old this month!
Category Theory in Idris
A new Statebox blogpost explaining programming languages as categories continues our series of category theory in Idris.
Spoiler alert: we have open sourced the category theory in Idris library! Check it out here. We look forward to your feedback and contributions!
New Paper: Computational Petri Nets
"Computational Petri Nets: Adjunctions Considered Harmful" investigates the link between Petri nets and free symmetric monoidal category from an applied perspective.
Abstract: We review some of the endeavors in trying to connect Petri nets with free symmetric monoidal categories. We give a list of requirement such connections should respect if they are meant to be useful for practical/implementation purposes. We show how previous approaches do not satisfy them, and give compelling evidence that this depends on trying to make the correspondence functorial in the direction from nets to free symmetric monoidal categories, in order to produce an adjunction. We show that dropping this immediately honors our desiderata, and conclude by introducing an Idris library which implements them.
Typedefs
Our satellite project Typedefs was trending this month as the most popular Idris repo.
We merged a big PR that implements term encoding and decoding, massive thanks to Fred for that! Typedefs can now convert typed terms into bytes and back again.
This month we also witnessed the first community contribution to the project,
PR#137, thanks a lot cb372!
Statebox Blogpost on Formal Verification
This new blogpost explains the novel approach to formal verification that Statebox is taking. A distiction between bottom-up and top-down formal verification is made, underlying the importance of category theory in achieving compositional code.
Statebox has built-in compositionality both within its code (which is written in Idris and verified bottom-up) and within its paradigm (programming with Statebox ensures a compositional bottom-up approach to verification).