TY  - RPRT
TI  - Experience Implementing a Performant Category-Theory Library in Coq
AU  - Jason Gross
AU  - Adam Chlipala
AU  - David I. Spivak
PY  - 2014
DO  - 10.1007/978-3-319-08970-6_18
UR  - https://arxiv.org/abs/1401.7694
ID  - 1401.7694
ER  -