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

Cur síos iomlán

Sonraí bibleagrafaíochta
Príomhchruthaitheoirí: Chlipala, Adam, Spivak, David I., Gross, Jason S.
Rannpháirtithe: Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science
Formáid: Alt
Teanga:en_US
Foilsithe / Cruthaithe: Springer-Verlag 2015
Rochtain ar líne:http://hdl.handle.net/1721.1/99929
https://orcid.org/0000-0002-9427-4891
https://orcid.org/0000-0001-7085-9417