CoqExtraction/Letouzey

#Certified functional programming Program extraction within Coq proof assistant

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.

…

##Syntactic conventions

• A presentation of Coq
• The extraction of Coq terms