[POPLmark] Re: adequacy

[Geoffrey A. Washburn]

On Mon, 9 May 2005, Robert Harper wrote:

> It is part of the statement of adequacy for an encoding to specify
> precisely what is meant by substitution / compositionality.  In the
> example below you are being mislead by the terminology.  The "leftist
> substitution" mentioned below would not be the substitution represented
> as such by the encoding.  Just because something is called substitution
> doesn't make it so!  BTW, there is no difficulty at all in formalizing
> lambda-circle in LF.

	If there is no difficulty I would appreciate it if I could see how
  you would do so.  Thanks!

-- 
-- Geoff Washburn | geoffw at cis.upenn.edu | http://www.cis.upenn.edu/~geoffw/ --