The \(HOL\) logic extended with quantification over type variables

DOI10.1007/BF01383982zbMath0785.68082OpenAlexW2997670298MaRDI QIDQ1309243

Thomas F. Melham

Publication date: 16 January 1994

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01383982

zbMATH Keywords

typestheorem provinghigher-order logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (1)

The HOL-Omega Logic

Uses Software

• ML
• HOL
• LCF

Cites Work

• Unnamed Item
• The system \({\mathcal F}\) of variable types, fifteen years later
• Edinburgh LCF. A mechanized logic of computation
• A transfinite type theory with type variables
• A formulation of the simple theory of types

This page was built for publication: The \(HOL\) logic extended with quantification over type variables