[POPLmark] how to believe a twelf proof

[Karl Crary]

This is a good question, but I believe I answered it fully in an earlier 
message, which I am attaching.

    -- Karl


Randy Pollack wrote:

>Karl,
>
>Okay, "sr" checks in every world for which the representations of
>"tp", "tm", "of" and "red" are adequate, so we can read "sr" as a
>theorem about the intended object language typing and reduction
>relations.  Am I right that this is your point?
>
>Similarly, Frank's proof of type preservation for cbv evaluation,
>which hapens to check in a closed world, also checks in every world
>for which the representations of "tp", "tm", "of" and "eval" are
>adequate, so we can read "sr" as a theorem about the intended object
>language typing and evaluation relations.
>
>Now we are getting to my real question.  In your PoplMark solution,
>file 1a.elf, the lemma "trans" does NOT check in every world in which
>"tp", "assm" and "sub" are adequate representations of the intended
>object language.  I believe you agreed with me in previous email that
>the world in which "tp", "assm" and "sub" are adequate representations
>is generated by the block
>
>  %block pure : some {t:tp} block {x:tp} {d:assm x t}.
>
>But "trans" also requires some other assumptions about "var" and
>"assm_var" to check.  So, why should I consider "trans" as a theorem
>about the intended object language subtyping relation???
>
>Randy
>
>  
>
-------------- next part --------------
An embedded message was scrubbed...
From: Karl Crary <crary at cs.cmu.edu>
Subject: Re: Twelf solution: adequacy theorem
Date: Thu, 28 Apr 2005 13:35:48 -0400
Size: 5534
Url: http://lists.seas.upenn.edu/pipermail/poplmark/attachments/20050513/1116add5/AttachedMessage.eml