Николай Иваныч (nivanych) wrote in category_theory,
Николай Иваныч
nivanych
category_theory

Category Theory in Coq 8.5

Category Theory in Coq 8.5
Amin Timany, Bart Jacobs
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.
http://arxiv.org/abs/1505.06430
Subscribe
  • Post a new comment

    Error

    default userpic

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 0 comments