Automath

Automath (pour ) était un langage formel, développé par Nicolaas Govert de Bruijn à partir de 1967, dont le but était d'exprimer des théories mathématiques complètes de manière à inclure un assistant de preuve qui pouvait en vérifier la correction. Le système Automath apportait de nombreuses notions novatrices qui ont été adoptées ou réinventées ultérieurement, comme la substitution explicite ou la notion de type dépendant dont Automath est un exemple paradigmatique. Automath était aussi le premier système pratique qui exploitait la correspondance de Curry-Howard. Les propositions étaient représentées comme les ensembles (appelées ) de leurs preuves, et le problème de l'existence de preuve se ramenait à tester la vacuité d'un ensemble ; de Bruijn ne connaissait pas les travaux de Howard, et a énoncé la correspondance indépendamment. Automath n'a pas été largement publié à l'époque, et n'a pas été utilisé à grande échelle ; mais c'est un système précurseur des assistants de preuve actuels.