[POPLmark] Experience report with Twelf

Karl Crary crary at cs.cmu.edu
Tue Aug 30 14:30:31 EDT 2005


Sure, we could stipulate that a program runs on an oracle machine that 
is capable of deciding undecidable problems.  We could work out the 
metatheory for the oracle version and it's easy to see how classical 
logic would arise in such an account.

However, I never thought the downcasting check in FJ was intended to 
require an oracle machine.  Rather, I took it as a technical shorthand 
for a dynamic check that really could be implemented.  (I am fairly 
certain that Benjamin intended it that way as well.)  If so, then 
proving that it actually can be is an essential part of the metatheory.  
Whether you prefer to call it part of "safety," I don't really care.

The only other option is to lay out the operational semantics in such a 
way that it shows how to do the downcasting check (presumably, using 
some sort of tagging regime).  If you do that, you're off the hook for 
the proof, but I don't see it as an option to do neither, unless you're 
embracing the oracle-machine interpretation.

    -- Karl


Steve Zdancewic wrote:

> I think Benjamin's point is that the definition of soundness makes no
>
>reference to the computability of the transition relation -- that is 
>something that you're imposing on the definitions with the added 
>condition that "a machine can find" the transition.  If I take the 
>definition of soundness literally, I don't see any "machine" mentioned 
>anywhere.
>
>Soundness makes perfect sense for languages that can't be implemented on 
>a Turing machine.  Whether or not such a thing is useful is another 
>matter...
>
>  
>


More information about the Poplmark mailing list