#Certified functional programming Program extraction within Coq proof assistant

[these_letouzey_English.ps.gz](http://www.pps.jussieu.fr/~letouzey/download/these_letouzey_English.ps.gz)

##Acknowledgments
##Introduction

###The need for certified programs
Today, it is obvious to say that software occupies a dominating place in our modern socienties, including in critical roles.
The list of these missions of confidence now filled by programs lengthens unceasingly.
It can be a matter of controlling high-risk equipments like planes or nuclear thermal power stations, but it can also be more prosaic operations like the management of electronic payments.
In any case, whether human lives or money are in questions, the stakes are huge.

...

### The Curry-Howard isomorphism
### The extraction in Coq
### The contributions of this thesis
#### Complete support of the universes
#### Solving the typing problems
#### Correctness of strict evaluation
#### Support of the system's evolutions
#### Modules and interfaces
#### Our contributions in brief
### Comparison with other extraction systems
#### Deletion of logical parts in proofs
#### Translation to a true functional language
### Summary

This work begins with a progressive introduction to the Coq proof assistant.
The first part of the chapter 1 presents via examples the principal features of this system, and in particular those which influence the extraction.
The second part of this chapter exposes more formally the CIC, which is Coq's underlying theoretical system.

After this brief review of Coq and CIC, we start a first half of this manuscript dedicated to the presentation of our new extraction.
The chapter 2 first of all present our redesign of the extraction function E for terms, and complementary two proofs of its correctness.
The first proof is syntactic proof stating that reduction of extracted terms cannot not fail, the second proof is a semantic proof ensuring the correctness of extracted terms with respect to theirs specifications.

The chapter 3 is then dedicated to the typing of the extracted terms.
We start by studying in detail, which kind of non-typability the extracted terms may presents in a ML-like typing system, then we propose a solution for skirting these difficulties.

Lastly, the chapter 4 supplements the description of our new extraction by presenting the last aspects of our work:
extraction of modules, of co-inductive types, of record types, and lastly optimization of the extracted code.
Finally we briefly present the implementation carried out, from both developer's and user's point of view.

The chapter 5 starts the second half of the manuscript, devoted to case studies.
In this chapter, we first review the users contributions from the point of view of extraction, these users contributions forming an already consequent library of examples of Coq developments.
Then we detail the case of two of these contributions, which put at fault the old extraction:
the first on exceptions by continuations, due to J.-F. Monin, and the second on Higman's lemma, by H. Herbelin.

The chapter 6 gives a progress report on an ambitious project consisting in developing a library of arithmetic real exact by extraction of a development of constructive real analysis.
The development in question if the C-CoRN project at the university of Nijmegen.
We will see that one is still far from the goal, but that at the same time enormous progress were already accomplished.
In addtion, we present a small alternative expreimentation around constructive reals made in collaboration with H. Schwichtenberg.

Lastly, the chapter 7 presents the certification of the Ocaml library of finite sets which we carried out in collaboration with J.-C. Filliatre.
This development is one of first to combine modules, functors and extraction.

##Syntactic conventions

- [A presentation of Coq](Letouzey/1)
- [The extraction of Coq terms](Letouzey/2)