Semantics for dependently-typed HOL

DOI10.1007/978-3-032-32592-1_9MaRDI QIDQ7411300zbMATH OpenFDO

Authors Florian Rabe

Publication date 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-32592-1_9

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A consistent foundation for Isabelle/HOL
• A formulation of the simple theory of types
• A simple type theory with partial functions and subtypes
• Categorical logic and type theory
• Completeness in the theory of types
• Dependently typed higher-order logic
• Experiments with choice in dependently-typed higher-order logic
• FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES
• Generalized algebraic theories and contextual categories
• HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 3999882 (Why is no real title available?)
• scientific article; zbMATH DE number 1863390 (Why is no real title available?)
• Kripke Semantics for Martin-L\"of's Extensional Type Theory
• Tableaux for automated reasoning in dependently-typed higher-order logic
• The HOL-Omega Logic
• The Lean theorem prover (system description)
• Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint
• THF0 – The Core of the TPTP Language for Higher-Order Logic

This page was built for publication: Semantics for dependently-typed HOL

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