in Uncategorized

A comparison of category theory software

The following table compares general and technical information for a number of existing and hypothetical category theory software packages. Drawn from the discussion (ft. Jamie Vicary) on May 1, 2018 at the Applied Category Theory workshop in Leiden.

Software packageDoes it exist?AuthorGoalUser interactionAutomationHow to define categoriesCategorical settingStructures it can computeArchitectureDirected? (i.e. categories vs. groupoids)
HoTT libraries in Cog or AgdaYesVariousResearchCodeProof assistantVia presentationsHigher (weak)Limits, colimits, functorsLibraryNo
OpetopicYesEric FinsterResearchGeometricallyNoneVia presentationsHigher (weak)LibraryYes
QuantomaticYesAleks Kissinger et al.Research, scale, interoperability (?)GeometricallyProof assistantVia presentationsStrict, symmetric monoidalStandaloneNo
Algebraic Query Language (AQL)YesRyan Wisnesky, David SpivakCommercial, teachingCodeQuery optimizer, data migrationExplicitly, and via presentationsMonoidalLimits, colimits, functorsStandalone + libraryYes
GlobularYesJamie Vicary et al.Research, publishingGeometricallyNoneVia presentationsHigher (semi-strict)StandaloneYes
TikZitYesAleks Kissinger et al.PublishingLaTeXNoneLibrary
TypedefsUnder developmentJelle Herold et al.CommercialCode
Proto-Quipper-MYesFrancisco Rios, Peter SelingerResearch
RholangUnder developmentMike Stay et al.Commercial
EASIKYesBob Rosebrugh et al.ResearchGeometrically
CatenoYesJason MortonResearch
PySheafYesMichael RobinsonResearchCode
SpecwareYesKestrel InstituteCommercial
CatlabUnder developmentEvan Patterson
OICOSUnder developmentViktor Winschel, Philipp ZahnCommercial
StateboxUnder developmentJelle Herold et al.Commercial
TikzWDYesPatrick Schulz, David SpivakPublishingLaTeX
DSL for OperadsNoTBDSimulationGeometricallyNoneVia presentationsOperadsStandalone
Common File Format for Categorical ConstructionsNoTBDInfrastructureCodeType-checkingExplicitly, or via presentationsAllFile format

The last two items in the table are “wish list” items identified by members of the ACT community.

Write a Comment

Comment