Category Theory in Coq 8.5
Logic in Computer Science
2015-05-26 v1
Abstract
We report on our experience implementing category theory in Coq 8.5. The repository of this development can be found at https://bitbucket.org/amintimany/categories/. This implementation most notably makes use of features, primitive projections for records and universe polymorphism that are new to Coq 8.5.
Cite
@article{arxiv.1505.06430,
title = {Category Theory in Coq 8.5},
author = {Amin Timany and Bart Jacobs},
journal= {arXiv preprint arXiv:1505.06430},
year = {2015}
}
Comments
This is the abstract for a talk accepted for a presentation at the 7th Coq Workshop, Sophia Antipolis, France on June 26, 2015