We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
An experimental library of formalized Mathematics based on the univalent foundations.
- Authors
VOEVODSKY, VLADIMIR
- Abstract
This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started to work on this library in February 2010 in order to gain experience with formalization of Mathematics in a constructive type theory based on the intuition gained from the univalent models (see Kapulkin et al. 2012).
- Subjects
PROOF theory; UNIVALENT functions; MATHEMATICS; TYPE theory; MATHEMATICAL models
- Publication
Mathematical Structures in Computer Science, 2015, Vol 25, Issue 5, p1278
- ISSN
0960-1295
- Publication type
Article
- DOI
10.1017/S0960129514000577