[POPLmark] Poplmark Digest, Vol 10, Issue 5

Karl Crary crary at cs.cmu.edu
Mon Jun 12 13:25:40 EDT 2006

Hi Michael,

I think it would be interesting to prove the sort of result you're 
talking about, although I would prefer not to overload the term 
"adequacy" to refer to it.  However, I'm curious why you think that no 
one would ever attempt to prove adequacy (in the usual sense) for an HOL 
encoding.  Is there some technical obstacle, or are you just saying that 
the HOL community isn't interested in that sort of thing?

    -- Karl Crary

Michael Norrish wrote:
> I don't think anyone would ever attempt the project you are describing
> for HOL.  Rather, we would prove what I think might be called an
> adequacy result entirely at the object level.  It is trivial to
> establish a type of first order, algebraic terms corresponding to the
> named syntax with explicit free variables, and not identified up to
> alpha-equivalence.  I think this is the type that we all accept as the
> fundamental bedrock, to which we can all revert if we must, however
> unpleasant its properties.  This is the type for which notions of
> recursion and induction are uncontroversial.

More information about the Poplmark mailing list