Mécanisation de la recherche de preuves et de programmes en arithmétique fonctionnelle du second ordre. (Mechanization of proof search for program synthesis in the second order functional arithmetic). - Odile Hermann (1995)