Showing 1–2 of 2 results for author: Perone, M

idris-ct: A Library to do Category Theory in Idris

Authors: Fabrizio Genovese, Alex Gryzlov, Jelle Herold, Andre Knispel, Marco Perone, Erik Post, André Videla

Abstract: We introduce idris-ct, a Idris library providing verified type definitions of categorical concepts.idris-ct strives to be a bridge between academy and industry, catering both to category theorists who want to implement and try their ideas in a practical environment and to businesses and engineers who care about formalization with category theory: It is inspired by similar libraries developed for t… ▽ More We introduce idris-ct, a Idris library providing verified type definitions of categorical concepts.idris-ct strives to be a bridge between academy and industry, catering both to category theorists who want to implement and try their ideas in a practical environment and to businesses and engineers who care about formalization with category theory: It is inspired by similar libraries developed for theorem proving but remains very practical, being aimed at software production in business. Nevertheless, the use of dependent types allows for a formally correct implementation of categorical concepts, so that guarantees can be made on software properties. △ Less

Submitted 14 September, 2020; v1 submitted 25 November, 2019; originally announced December 2019.

Comments: In Proceedings ACT 2019, arXiv:2009.06334

Journal ref: EPTCS 323, 2020, pp. 246-254

Computational Petri Nets: Adjunctions Considered Harmful

Authors: Fabrizio Genovese, Alex Gryzlov, Jelle Herold, Marco Perone, Erik Post, André Videla

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 directio… ▽ More 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. △ Less

Submitted 8 May, 2019; v1 submitted 29 April, 2019; originally announced April 2019.

Comments: 29 Pages, 6 Figures, 1 Listing