Abstract
The goal of this paper is to report on a formalization of the p-adic numbers in the setting of the second author's univalent foundations program. This formalization, which has been verified in the Coq proof assistant, provides an approach to the p-adic numbers in constructive algebra and analysis.
Cite
CITATION STYLE
APA
Pelayo, Á., Voevodsky, V., & Warren, M. A. (2015). A univalent formalization of the p-adic numbers. Mathematical Structures in Computer Science, 25(5), 1147–1171. https://doi.org/10.1017/S0960129514000541
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
Already have an account? Sign in
Sign up for free