Des logiques d'ordre supérieur à la programmation vérifiée en Coq