The Coq mailing list

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

Hi Randy,

>I think that is slightly misleading.  For adequacy of HOAS
>representation you need termination of the meta language,
>which seems to require types.

Automath is very much a typed system, no problem there.

>You also need to identify meta language terms up to
>beta-eta-conversion.  What is the deal with Automath and eta?

The original Automath had eta, but for formalization
of mathematics eta turned out not to be very important.
I don't know whether there have been Automaths without eta.

How much of the metatheory has been properly worked out to
back my claims I don't know.  Probably more than I know of,
but probably less than would satisfy you.  Also there have
been all kind of variants of Automath, some of them quite
baroque.  I think the Automath best suited for a logical
framework and closest to lambda-P was AUT-68.

The person to ask about this was Bert Jutting, but he isn't
there anymore.

Freek