The HOL logic extended with quantification over type variables
| Author(s) : | Thomas F. Melham, |
| Publisher : | N/A |
| Publication Date : | 1993 |
| ISSN : | N/A |
| Abstract : | This paper discusses a proposal to extend the primitive basis of the HOL logic with a very simple form of quantification over types. It is shown how certain practical problems with using the definitional mechanisms of HOL would be solved by the additional expressive power gained by making this extension., |