P. MANOURY Preuve de correction de programmes fonctionnels de tris dans le systèmes Coq Ce rapport présente une étude de cas de preuve de correction de programmes fonctionnels. Tous les programmes, spécification et preuves ont était développés à l'aide du système d'aide à la démonstration Coq. Les programmes étudiés sont des im­ plémentations de divers algorithmes de tri. Ce document contient les définitions des structures de données utilisées dans les algorithmes de tri (listes et arbres binaires) et de leurs propriétés attendues. Quelques fonctions auxiliaires sont données ainsi que les propriétés concernant leur usage dans des programmes de tri. Nous définissons ensuite nos divers pro­ grammes de tri et décrivons les grandes lignes de leurs preuves de correction. Nous avons étudié cind programmes : le tri par in­ sertion, le tri par funsion, le tri par arbre binaire de recherche, le tri par tas et le tri-bulle. En supplément nous donnons la preuve de correction d'une fonction calculant des ar­ bre binaires équilibrés utilisée dans les tris par fusion et par tas. L'intérêt de ce rapport vaut moins par l'originalité de ses résultats (les algorithmes présentés sont bien connus) que par son effectivité. Enfin, ce document peut être utilisé comme une bonne introduction pédagogique à la problématique de la correc­ tion des programmes. This report is a case study in proving correctness of function­ al programs. All programs specifications and proofs has been de­ veloped with the Coq proof assistant. The programs investigated are implmentions of variuos sorting algorithm. The document contains the definitions of data structures in­ volved in sorting programs (lists and binary trees) and their in­ tended properties. Some auxiliary functions are defined and their properties concerning their use in sorting programs are stated. Then we define our various sorting programs and give the broad outlines of the proof of their correctness. We studied five sort­ ing programs : insertion sort, merge sort, binary search tree and heap sorts, bubble sort. As an extra we give the corectness proof of a function building well balanced trees which is used in merge and heap sorts. The interest of this report is not in its originality (sorting algorithm we present are well known) but merely in its actuality. Also it appears that this document is a good pedagogical intro­ duction to the problematic of programs correctness.