19 citations · 60 across the 11 of their papers we have counts for
3 papers · 2 filters
From signatures to monads in UniMath
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core depend…
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…
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…