Les travaux en logique pure constituent l'autre moteur de la renaissance des types . Une renaissance portée par la découverte à la fin des années 1960 d'une profonde correspondance entre les programmes informatiques et les démonstrations mathématiques , la « correspondance de Curry-Howard » . Cette correspondance stipule qu'en utilisant le langage des types , les preuves peuvent se lire comme des programmes . Le langage inventé par Russell est alors mûr pour sortir du bois . Plusieurs théories des types sont imaginées , comme le très élégant système F du logicien Jean-Yves Girard . Mais c'est finalement le Suédois Per Martin-Löf qui élabore , dans les années 1970 , la théorie des types que nous connaissons aujourd'hui . Un formalisme conçu pour mettre en pratique la correspondance preuve-programme . Un pas décisif sera réalisé dans les années 1980 par deux informaticiens français : Gérard Huet et son étudiant en thèse Thierry Coquand . » Avec notre calcul des constructions' , nous cherchions comment utiliser la théorie des types pour représenter des preuves mathématiques sur ordinateur , mais aussi pour développer des programmes , raconte Thierry Coquand . Nous voulions un formalisme qui fonctionne pour représenter à la fois des preuves mathématiques et des programmes , avec l'idée , sans doute un peu naïve alors , d'unifier mathématiques et informatique . » L'assistant de preuve ainsi conçu , baptisé Coq par Gérard Huet , va se révéler très efficace . Il permettra en 2005 à l'équipe de Georges Gonthier et Benjamin Werner de vérifier sur ordinateur un théorème fameux , bien que secondaire , le « théorème des quatre couleurs » ( voir p . 117 ) . Puis , en 2012 , le théorème de Feit-Thompson , un résultat de l'algèbre du siècle cette fois-ci majeur ( voir S&V n° 1148 , p . 82 ) . » Ce qu'a fait Georges Gonthier est pour moi un bon exemple d'unification entre mathématique et informatique , car il a dû réexprimer des concepts mathématiques de manière informatique . Et cela a été utile pour avoir de meilleures preuves « , estime Thierry Coquand . Reste à voir si tout le reste des mathématiques se laisse aussi traduire à l'aide de la théorie des types .