[TYPES] how to typing for logic equality operator

[Derek Dreyer]

Yes, Moez, this would appear to be a typo.  The typo is corrected in
the presentation of FJ in Pierce's TAPL book (Theorem 19.5.4,
Progress).

Derek

> Incidentally, it seems there is a minor (but embarrassing?) typo in the FJ paper (only in the TOPLAS version).
>
> The flaw, in Theorem 2.4.3 (FJ Type Soundness), on p. 408, is in the last part of the theorem stating that 'C <: D'.
>
> I believe there must be a 'not' (/) over the '<:' symbol.  Otherwise (ie, if the condition as stated is true), the (up-)cast subexpression could simply evaluate/reduce to 'new C([e])', and would not be a failing typecast (as explained close to the end of p.401).
>
> The same error is repeated in Theorem 3.4.3 (FGJ Type Soundness), I believe, for 'Phi |- N <: P', on p. 415.
>
> Or am I missing something?
>
> -Moez
>