1998: David présente en exposé dans le cours de Giuseppe Longo la preuve de la normalisation forte du Système F par le témoins de réducibilité (je n'ai pas poussé l'abnégation jusqu'à faire celle du Calcul des Constructions).

2009: David prépare un cours de langages de programmation et se rend compte qu'il a tout oublié de ladite preuve de normalisation forte. David révise.

2015: David entend parler d'un truc chelou sur Fω et essaye, sans succès, de se rappeler pourquoi F est fortement normalisant.

Il faut se rendre à l'évidence, David ferait mieux d'essayer d'arrêter de comprendre grand chose à la théorie des types. Ou du moins de tenter de s'en rappeler plus que fugacement.