The HOL logic extended with quantification over type variables

DOI10.1007/BF01383982zbMATH Open0785.68082OpenAlexW2997670298MaRDI QIDQ1309243FDOQ1309243

Authors: 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

Recommendations

• Quantified multimodal logics in simple type theory
• (In)consistency of Extensions of Higher Order Logic and Type Theory
• Higher-Order Logic and Type Theory
• scientific article; zbMATH DE number 2110621
• Stateless higher-order logic with quantified types
• Logical relations and the typed λ-calculus
• scientific article; zbMATH DE number 516994
• scientific article; zbMATH DE number 3273876
• scientific article; zbMATH DE number 1984270
• scientific article; zbMATH DE number 139986

zbMATH Keywords

typestheorem provinghigher-order logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• Title not available (Why is that?)
• Edinburgh LCF. A mechanized logic of computation
• The system \({\mathcal F}\) of variable types, fifteen years later
• A formulation of the simple theory of types
• A transfinite type theory with type variables

Cited In (9)

• From types to sets by local type definition in higher-order logic
• An extension of the Boyer-Moore theorem prover to support first-order quantification
• Importing mathematics from HOL into Nuprl
• The HOL-Omega Logic
• Title not available (Why is that?)
• The addition of bounded quantification and partial functions to a computational logic and its theorem prover
• Stateless higher-order logic with quantified types
• HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism
• Abstract deduction and inferential models for type theory

Uses Software

• ML
• HOL
• LCF

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1309243)