Constructive real analysis : a type-theoretical formalization and applications
Cruz Filipe, Luís Calhorda · 2004
This thesis is concerned with the formalization of mathematics in the proof assistant Coq, in particular the formalization of Bishop's constructive development of Real Analysis. In order to do this, serious thought had to be given to several important issues which had not previously been addressed in this context, namely the representation of concepts and the construction of auxiliary tools to help developing the proofs. The formalization is the departure point to more general considerations on how a large library should be developed and organized so that its contents can be easily accessed and used by others. The work described in this thesis can be summarized in three points: - construction of the C-CoRN library (formalization of Real Analysis and development of tactics); - development of a working methodology; - applications to program extraction (case study: extracting and optimizing a program from the formalized library). The thesis ends with a general overview of what was achieved and some concluding remarks. A short introduction to Coq is provided in the Appendix. The whole formalization, together with the documentation, can be accessed via the C-CoRN home page, http://c-corn.cs.kun.nl/.