Experience Implementing a Performant Category-Theory Library in Coq

Experience Implementing a Performant Category-Theory Library in Coq

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 proo...

Full description

Bibliographic Details
Main Authors: Chlipala, Adam (Contributor), Spivak, David I. (Contributor), Gross, Jason S. (Contributor)
Other Authors: Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science (Contributor), Massachusetts Institute of Technology. Department of Mathematics (Contributor)
Format: Article
Language:English
Published: Springer-Verlag, 2015-11-13T16:55:46Z.
Subjects:
Article
Online Access:Get fulltext

Internet

Get fulltext

Similar Items