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:

• It is fast. It is 30 times as fast as Mizar, which itself is 30 times as fast as Coq. On a 1GHz machine it will check the full Jutting formalization (about 750K of Automath source) in 0.5 seconds.
• Its implementation of lambda terms doesn't use named variables or de Bruijn indices (the two common approaches) but instead uses a directed graph representation. In this, bound variables are represented by pointers to a lambda.

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

http://www.cs.kun.nl/~freek/aut/.