[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Jevgenijs Sallinens]

Quoting Hongwei Xi <hwxi at cs.bu.edu>:

> I would like to point out that for a system like ATS/LF, the justification
> for adequacy (when HOAS is involved) only relies on the strong 
> normalization and Church-Rosser properties of the simply typed lambda 
> calculus. 

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/