[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Michael Norrish]

Karl Crary writes:
 
> However, no matter how you decide to state adequacy, you are still
> ultimately trying to provide an isomorphism between the object
> language and some concept in the meta-language.  That means that you
> are going to need some strategy for dealing with the meta-language's
> proof theory.  At the very least you will need consistency, or the
> meta-language tells you nothing at all.

Perhaps your definition of adequacy requires the involvement of a
meta-language.  I think there's still an interesting question to be
asked even in its absence however (as spelt out in my earlier
message).

In particular, the HOL approach's strength is that a quotiented,
identified-up-to-alpha equivalence representation is just as much at
the object level as is the algebraic representation.  So too is the
Weak HOAS representation.  (Work by Ambler et al suggests Strong HOAS
is also possible.)  This allows one to reason mechanically about the
inter-relationships between all of them.

Michael.