Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers
This paper describes a formalization of the first book of the series ``Elements of Mathematics'' by Nicolas Bourbaki, using the Coq proof assistant. In a first paper published in this journal, we presented the axioms and basic constructions (corresponding to a part of the first two chapt...
Main Author: | |
---|---|
Format: | Article |
Language: | English |
Published: |
University of Bologna
2016-12-01
|
Series: | Journal of Formalized Reasoning |
Subjects: | |
Online Access: | https://jfr.unibo.it/article/view/4771 |