[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Karl Crary]

I think this question pithily summarizes the point under debate.  My 
position is that whenever we encode a formal system in a metalanguage, 
we should prove that the encoding is isomorphic to the original system.  
Some seem to feel that if you are using first-order encodings, adequacy 
is too trivial to bother doing.  I'm arguing that, to the contrary, the 
proof-theory of the metalanguage has much more of an impact on the 
adequacy proof than your strategy for dealing with binding.

    -- Karl


Jevgenijs Sallinens wrote:
> Hi,
> Is it correct that need for 'adequacy' depends on if HOAS is involved?
> Seems, Karl is speaking about this case, but Daniel and Michael about 
> establishing equivalence between different encodings withing same or different 
> LF, when no need to bother about HOAS assumptions.
> In the last case strong normalizations required to ensure consistency, but 
> according to Goedel we couldn't proof consistency within the system itself.
> Best Regards,
>
> -- Jevgenijs Sallinens
>
>
> -------------------------------------------------
> This mail sent through IMP: http://webmail.dva.lv/
>
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>
>