Prouver les programmes : pourquoi, quand, comment ?

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