Experience implementing a performant category-theory library in Coq

DOI10.1007/978-3-319-08970-6_18zbMATH Open1416.68163arXiv1401.7694OpenAlexW2181522451MaRDI QIDQ2879258FDOQ2879258

Authors: Jason Gross, Adam Chlipala, David I. Spivak 

Publication date: 8 September 2014

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Abstract: We describe our experience implementing a broad category-theory library in Coq. Category theory and computational performance are not usually mentioned in the same breath, but we have needed substantial engineering effort to teach Coq to cope with large categorical constructions without slowing proof script processing unacceptably. In this paper, we share the lessons we have learned about how to represent very abstract mathematical objects and arguments in Coq and how future proof assistants might be designed to better support such reasoning. One particular encoding trick to which we draw attention allows category-theoretic arguments involving duality to be internalized in Coq's logic with definitional equality. Ours may be the largest Coq development to date that uses the relatively new Coq version developed by homotopy type theorists, and we reflect on which new features were especially helpful.

Full work available at URL: https://arxiv.org/abs/1401.7694

Recommendations

• Category theory in Coq 8.5
• Developing the algebraic hierarchy with type classes in Coq
• A mechanically assisted constructive proof in category theory
• Type classes for mathematics in type theory
• A Coq formalization of finitely presented modules

zbMATH Keywords

performancedualitycategory theoryCoqhomotopy type theory

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to category theory (18-04)

Cited In (7)

• Mac Lane's comparison theorem for the Kleisli construction formalized in Coq
• Formal categorical reasoning
• Title not available (Why is that?)
• A trustful monad for axiomatic reasoning with probability and nondeterminism
• Category theory in Coq 8.5
• A mechanically assisted constructive proof in category theory
• A formalized hierarchy of probabilistic system types. Proof pearl

Uses Software

• Coq

This page was built for publication: Experience implementing a performant category-theory library in Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2879258)