[POPLmark] how to believe a twelf proof

[Karl Crary]

Oops, that's an editing bug.  That sentence should be struck.  Thanks.

    -- Karl


Randy Pollack wrote:

>Bob and Karl,
>
>A possibly trivial question about your note.  On p. 3 it says "Rather
>than specify base types, we will instead consider types with free type
>variables."  (I suppose "types" here means "object language types".)
>The Twelf signature immediately below does specify a base type
>
>  o : type.
>
>I suppose there could still be free type variables, but on p. 4 the
>world for adequacy of the representation of types is given as empty.
>Doesn't that mean no free type variables?
>
>Randy
>_______________________________________________
>Poplmark mailing list
>Poplmark at lists.seas.upenn.edu
>http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>
>
>  
>