Lists (2)
Stars
8
stars
written in Coq
Clear filter
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Metaprogramming, verified meta-theory and implementation of Coq in Coq
The mathematical study of type theories, in univalent foundations
A formalization of the textbook Elements of Set Theory
The TacTok automated Coq proof script synthesis tool
Formalization of the Introduction to Homotopy Type Theory in Coq
Formalisation of an affine type and effect system for a language with effect handlers