Experience Implementing a Performant Category-Theory Library in Coq
From MaRDI portal
Publication:2879258
DOI10.1007/978-3-319-08970-6_18zbMath1416.68163arXiv1401.7694OpenAlexW2181522451MaRDI QIDQ2879258
Jason Gross, Adam Chlipala, David I. Spivak
Publication date: 8 September 2014
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1401.7694
Related Items
A Formalized Hierarchy of Probabilistic System Types ⋮ Formal categorical reasoning ⋮ Mac Lane's comparison theorem for the Kleisli construction formalized in Coq ⋮ Unnamed Item ⋮ A trustful monad for axiomatic reasoning with probability and nondeterminism
Uses Software
