Experience Implementing a Performant Category-Theory Library in Coq.

Jason Gross Adam Chlipala David I. Spivak

Published in: ITP (2014)

Keyphrases

formal methods
theoretical framework
data mining
theoretical basis
database
efficient implementation
theorem prover
general theory