[POPLmark] Meta-comment

[danwang at CS.Princeton.EDU]

Let me make this analogy with call-cc. One certianly does not need to use call-
cc at all, just CPS convert your entire program! 

Twelf allows for nice proofs, because it offers many advanced features that can 
be used to encode object logics. Of course you don't have to use any of them, 
but that just defeats all the reasons to use Twelf.

Personally, If I wanted to use first-order encodings I might as well be using, 
Coq, Isabell, or HOL. They are more mature than Twelf and I'd say more 
appropiate for first-order encodings. 

I was not aware of the linearity encoding trick, but although it works. It 
would be much nicer and consistent with the Twelf/LF philsophy to have direct 
support.

Quoting Robert Harper <rwh at cs.cmu.edu>:

> Hi Dan,
> 
> Your message contains two misconceptions that are rather common, so 
> forgive me for correcting them here.
> 
> First, one can perfectly well encode linear logic in LF without having 
> any notion of linear function.  In fact this was one of the earliest 
> "test cases" for LF that we used way back when.  The trick is to take 
> advantage of the explicit representation of derivations as terms 
> provided by the LF methodology, and to introduce a judgement saying 
> that "this is a linear derivation".
> 
> Second, you seem to confuse the possibility of doing something (using 
> higher types to represent binders) with the necessity of doing so 
> (precluding the use of deBruijn indices, for example).  You can 
> perfectly well use first-order representations to encode a logic in LF, 
> if you so desire or are otherwise compelled to do so.  However, it 
> benefits you greatly (and, experience has shown time and again, it 
> benefits the encoded logic greatly) to try to take advantage of 
> built-in faciltiies such as higher types.  In practice you usually do, 
> and it's rarely an obstacle in and of itself.
> 
> Bob
> 

-------------------------------------------------
This mail sent through IMP: http://horde.org/imp/