English

Experimental library of univalent formalization of mathematics

History and Overview 2014-07-01 v2 Logic
Authors: Vladimir Voevodsky
View on arXiv ↗ PDF ↗

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.

Keywords

formalized mathematics Coq proof assistant univalent foundations mathematical library formalization

Cite

@article{arxiv.1401.0053,
  title  = {Experimental library of univalent formalization of mathematics},
  author = {Vladimir Voevodsky},
  journal= {arXiv preprint arXiv:1401.0053},
  year   = {2014}
}

Related papers

View all related →
Logic · Mathematics
A preliminary univalent formalization of the p-adic numbers
Álvaro Pelayo, Vladimir Voevodsky, Michael A. Warren
2013-02-07
Logic in Computer Science · Computer Science
Machine-Checked Categorical Diagrammatic Reasoning
Benoît Guillemet, Assia Mahboubi, Matthieu Piquerez
2024-03-01
Logic in Computer Science · Computer Science
The HoTT Library: A formalization of homotopy type theory in Coq
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman +2
2017-05-02
Computation and Language · Computer Science
Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs
Garett Cunningham, Razvan C. Bunescu, David Juedes
2023-01-06
Mathematical Software · Computer Science
Computer validated proofs of a toolset for adaptable arithmetic
Sylvie Boldo, Marc Daumas, Claire Moreau-Finot, Laurent Thery
2007-05-23
Digital Libraries · Computer Science
Large Formal Wikis: Issues and Solutions
Jesse Alama, Kasper Brink, Lionel Mamane, Josef Urban
2011-07-27
Formal Languages and Automata Theory · Computer Science
Formalization of closure properties for context-free grammars
Marcus V. M. Ramos, Ruy J. G. B. de Queiroz
2015-06-11
Logic in Computer Science · Computer Science
Trocq: Proof Transfer for Free, With or Without Univalence
Cyril Cohen, Enzo Crance, Assia Mahboubi
2024-02-21
Logic in Computer Science · Computer Science
Coquet: a Coq library for verifying hardware
Thomas Braibant
2011-08-23
Software Engineering · Computer Science
Plotting in a Formally Verified Way
Guillaume Melquiond
2021-08-10
Logic in Computer Science · Computer Science
Formalizing May's Theorem
Kwing Hei Li
2022-10-12
Logic · Mathematics
Set-theoretical mathematics in Coq
Carlos Simpson
2009-09-29
Logic in Computer Science · Computer Science
Reliably Reproducing Machine-Checked Proofs with the Coq Platform
Karl Palmskog, Enrico Tassi, Théo Zimmermann
2022-03-21
Logic in Computer Science · Computer Science
Mechanizing Matching Logic In Coq
Péter Bereczky, Xiaohong Chen, Dániel Horpácsi, Lucas Peña +1
2022-09-22
Data Structures and Algorithms · Computer Science
A Formalisation of Algorithms for Sorting Network
Laurent Théry
2022-03-04
Logic in Computer Science · Computer Science
The Lean mathematical library
The mathlib Community
2020-01-28
Logic in Computer Science · Computer Science
Computable analysis and notions of continuity in Coq
Florian Steinberg, Laurent Thery, Holger Thies
2023-06-22
Formal Languages and Automata Theory · Computer Science
Context-Free Language Theory Formalization
Marcus Vinícius Midena Ramos, Ruy J. G. B. de Queiroz
2015-05-04
Logic in Computer Science · Computer Science
Certified Exact Transcendental Real Number Computation in Coq
Russell O'Connor
2010-08-04
Logic in Computer Science · Computer Science
Experiences from Exporting Major Proof Assistant Libraries
Michael Kohlhase, Florian Rabe
2020-05-12
Logic in Computer Science · Computer Science
Formal Proofs of Transcendence for e and $\pi$ as an Application of Multivariate and Symmetric Polynomials
Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub
2015-12-10
Logic in Computer Science · Computer Science
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
Assia Mahboubi, Cyril Cohen
2015-07-01
Logic in Computer Science · Computer Science
Taming Differentiable Logics with Coq Formalisation
Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz +1
2024-07-08
History and Overview · Mathematics
Anatomy of a Formal Proof
Jeremy Avigad, Johan Commelin, Heather Macbeth, Adam Topaz
2024-11-20
Logic in Computer Science · Computer Science
A Survey of Languages for Formalizing Mathematics
Cezary Kaliszyk, Florian Rabe
2020-05-27