[POPLmark] Experience report with Twelf

[Brian E. Aydemir]

On 30 Aug 2005, at 15:52, Jevgenijs Sallinens wrote:

> As I suspect (nobody answered my previous e-mail in that respect),  
> F-sub  described in the challenge is exactly the same proven by  
> Benjamin to be undesidable (for subtyping (and therefore for  
> typing) relation).

Right.  Benjamin proved that the subtyping and typing relations of  
pure F-sub (without records) are undecidable, and the result carries  
over to F-sub extended with records.


> This lloks basicly making impossible to present solution for  
> problem 2 of challenge 3 (at least with Coq), since reflexive- 
> transitive closure of evaluation relation could not be given as  
> always terminating total computable function (to be presented in  
> Coq with fixpoint definitions).

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.

-Brian