The UniMath library for type theory and programming languages
Abstract
UniMath is a language for univalent formalization of mathematics as well as a library of formalized mathematics written in this language. This language is a subset of the language of the Coq proof assistant. The UniMath library was started by Vladimir Voevodsky in 2010 under the name Foundations. Since then it has passed what might be called the period of initial development. Today, UniMath contains a sufficient amount of basic mathematical knowledge to make it a useful resource for various formalization projects. The proposal outlined below concentrates on the UniMath-based work in two important directions - the study of categorical structures of dependent type theories and modeling of syntax and semantics of simple programming languages.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Apr 09, 2018
- Source ID
- FA95501710363
Entities
People
- Robert Macpherson
Organizations
- Air Force Office of Scientific Research
- Institute for Advanced Study
- United States Air Force