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...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Springer-Verlag
2015
|
| Online Access: | http://hdl.handle.net/1721.1/99929 https://orcid.org/0000-0002-9427-4891 https://orcid.org/0000-0001-7085-9417 |