Journal ArticleOPEN ACCESS

A univalent formalization of the p-adic numbers

Mathematical Structures in Computer Science (2015) 25(5) 1147-1171
DOI: 10.1017/S0960129514000541
15Citations
Citations of this article
9Readers
Mendeley users who have this article in their library.

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?

Save time finding and organizing research with Mendeley

Sign up for free