[POPLmark] Meta-comment

[Karl Crary]

Daniel C. Wang wrote:

> Users are of course also "stuck" if the metalogic is not rich enough 
> to reflect some of their object logic properties.  


I'm afraid I haven't any idea what this means.

> For example to encode linear logics in a way the reuses the binding of 
> the Twelf/LF metalogic requires extending the notion of Twelf/LF 
> function space to include linear functions.
>

With all the traffic, I can understand you missing this, but I pointed 
out earlier that this is not true.  LF can encode linear logics without 
any extension.


> Twelf/LF in nice because many things are "baked in". So long as those 
> things are the right things to bake in everyone is happy. However, I 
> think someone people are worried that they might want to step out of 
> the what is baked in Twelf.
>

What is baked in to LF are the notions of binding, alpha-equivalence, 
and substitution.  I don't think I'm going out on a limb to say that of 
all ideas in PL, these are the most standardized.  While it's true that 
this makes Twelf unsuitable for dealing with languages where 
substitution is broken (eg, early versions of Lisp), I hardly see this 
as a serious limitation.

    -- Karl