Article contents
A univalent formalization of the p-adic numbers
Published online by Cambridge University Press: 13 February 2015
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.
- Type
- Paper
- Information
- Copyright
- Copyright © Cambridge University Press 2015
References
- 4
- Cited by