Abstract: A contemporary implementation of Automath

Freek Wiedijk

his talk presents "aut", a modern Automath checker. It is a straight-forward reimplementation of the Zandleven Automath checker from the seventies. It was implemented about five years ago in the programming language C. It knows both the AUT-68 and AUT-QE dialects of Automath. This program was written to restore a damaged version of Jutting's translation of Landau's "Grundlagen".

Some noticable features:

The program has the feature that it can compile an Automath text into one very big "Automath Single Line" style lambda term. It outputs such a term using de Bruijn indices. (These lambda terms cannot be checked by modern systems like Coq or Agda, because the lambda-typed lambda calculi of de Bruijn are "incompatible" with the Pi-typed lambda calculi of modern type theory.)

The source of "aut" is freely available on the Web through