Experimental library of univalent formalization of mathematics

2013/12/30 by Vladimir Voevodsky, Voevodsky, Vladimir · 2 citations
Computer Science · Mathematics · #Logic, programming, and type systems #History and Theory of Mathematics #Computability, Logic, AI Algorithms

paper · pdf · doi:10.48550/arxiv.1401.0053

Abstract

This paper contains a discussion of a library of formalized mathematics for the proof assistant Coq which the author worked on in 2011-13.

Citations

• The Simplicial Model of Univalent Foundations (after Voevodsky)

Cited by

• The HoTT Library: A formalization of homotopy type theory in Coq
• Weakly globular Tamsamani N-categories and their rigidification

Related

• Reliably Reproducing Machine-Checked Proofs with the Coq Platform
• Anatomy of a Formal Proof
• Mathematical Logic: Proof Theory, Constructive Mathematics
• Automatically Proving Mathematical Theorems with Evolutionary Algorithms and Proof Assistants
• Recycling Proof Patterns in Coq: Case Studies