Rob, Peter: Peter Andrews' PhD thesis, supervised by Church and published by North-Holland in 1965, describes a simple type theory called "Q" that definitely includes object-language type variables. In fact Q also includes object-language universal quantification over these variables.
Tom ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
