Developing the theory and applications of SDCPNs to make real world impact.

The original GLAIVE Mission: to build a type theory and programming language where types are categories and dependent types are fibrations. Bold experiments in syntax and an advising role on the type theory for learners project.

Agda as a blackboard for

• Making Flavoured Petri nets more type theoretic (Coloring in Poly?)
• The modal Mu-calculus for Coloured Petri nets
• Fresh Petri nets! Nets based on fresh lists.

Aims to utilize the vast categorical work in 1Lab and ROCQ to build a type theory for reasoning logically about learners. Developing a type theory that will be

• multimodal/fibrational
• substructural and partially cartesian
• based on the internal logic of Poly
• not extensional!

Aims to develop software and theory for SDCPN simulation which

• provides a reference implementation for the other SGAI platforms
• Performs safety analysis via:
• Monte Carlo simulation
• Probabilistic control theory

Aims to develop a notion of bisimulation up to epsilon between SDCPNs and ordinary stochastic Petri nets. We also aim to develop a stone duality allowing for minimization of a flavored Petri net into simplest form and to develop a categorical perspective on region theory. These theoretical results will allow the SDCPN engine to utilize standard Petri net model checking tools and we have plans to integrate PRISM into the engine.