The Coq mailing list

[Freek Wiedijk <freek AT cs.ru.nl>]

Hi Yasuaki and Yves,

>If I remember correctly, early version of Automath
>(starting around 1968 and into the 1970s) used lambda
>terms to describe the type of lambda terms.

*All* versions of Automath.  In Automath there has never
been a difference between lambda and Pi, both "fun x :
A =>" and "forall x : A," are written as [x:A].  You get
very nice typing rules that way:

        Gamma |- M : A   Gamma |- N : B
        -------------------------------
               Gamma |- MN : AN

             Gamma, x : A |- M : B
            ------------------------
            Gamma |- [x:A]M : [x:A]B

But of course Automath still has the ugliness of the
conversion rule, so nothing is perfect :-)

Freek