45 citations · 80 across the 5 of their papers we have counts for
Showing 2016Show all
2 papers · 1 filter
cs.LO2016★ 10 cited
Cubical Type Theory: a constructive interpretation of the univalence axiom
Cyril Cohen, Thierry Coquand, Simon Huber +1
This paper presents a type theory in which it is possible to directly manipulate -dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent…
cs.LO2016★ 13 cited
Formalized linear algebra over Elementary Divisor Rings in Coq
Guillaume Cano, Cyril Cohen, Maxime Dénès +2
This paper presents a Coq formalization of linear algebra over elementary divisor rings, that is, rings where every matrix is equivalent to a matrix in Smith normal form. The main…