[POPLmark] Experience report with Twelf

Karl Crary crary at cs.cmu.edu
Wed Aug 31 16:55:43 EDT 2005


I believe this misses the point entirely.  The downcasting check in FJ 
is--in fact--decidable; I don't believe anyone has contested that.  
However, Stephanie's opening claim was that it is too hard to *prove* 
that it is decidable.  If that is so, then to be honest we should look 
at the downcasting check as if it were undecidable, regardless of the 
facts of the matter.

    -- Karl

Brian E. Aydemir wrote:

> Unlike in Featherweight Java, a derivation of "t1 --> t2" in F-sub
>
>does not require the construction of any subtyping derivations.   
>Thus, the undecidability of the subtyping and typing relations does  
>not necessarily imply that the evaluation relation is also undecidable.
>
>  
>



More information about the Poplmark mailing list