A Brief Overview of HOL4

DOI10.1007/978-3-540-71067-7_6zbMath1165.68474OpenAlexW1943070836MaRDI QIDQ3543646

Publication date: 4 December 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71067-7_6

Mathematics Subject Classification ID

Related Items

The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ On definitions of constants and types in HOL ⋮ Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation ⋮ Automatic Proof and Disproof in Isabelle/HOL ⋮ Formalization of linear space theory in the higher-order logic proving system ⋮ The role of entropy in guiding a connection prover ⋮ AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code ⋮ Aligning concepts across proof assistant libraries ⋮ Formalization of reliability block diagrams in higher-order logic ⋮ Proof producing synthesis of arithmetic and cryptographic hardware ⋮ Computer assisted reasoning. A Festschrift for Michael J. C. Gordon ⋮ Hammer for Coq: automation for dependent type theory ⋮ Formally verified algorithms for upper-bounding state space diameters ⋮ Extensional higher-order paramodulation in Leo-III ⋮ A mechanisation of some context-free language theory in HOL4 ⋮ Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems ⋮ Proof-Producing Reflection for HOL ⋮ Pattern Matches in HOL: ⋮ A formalized general theory of syntax with bindings ⋮ Formalization of functional variation in HOL Light ⋮ Tactics for hierarchical proof ⋮ Unnamed Item ⋮ Theoretical and practical approaches to the denotational semantics for MDESL based on UTP ⋮ Quantified multimodal logics in simple type theory ⋮ Parameterized synthesis for fragments of first-order logic over data words ⋮ Function extraction ⋮ Monotonicity inference for higher-order formulas ⋮ Analytic tableaux for higher-order logic with choice ⋮ Formal reasoning under cached address translation ⋮ Unnamed Item ⋮ Psi-calculi in Isabelle ⋮ Unique solutions of contractions, CCS, and their HOL formalisation ⋮ Friends with Benefits ⋮ The CADE-27 Automated theorem proving System Competition – CASC-27 ⋮ A Verified Compositional Algorithm for AI Planning ⋮ \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ A verified proof checker for higher-order logic ⋮ Highly Automated Formal Proofs over Memory Usage of Assembly Code ⋮ The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4 ⋮ Transforming Programs into Recursive Functions ⋮ Monotonicity Inference for Higher-Order Formulas ⋮ From LCF to Isabelle/HOL ⋮ Formalization of Euler-Lagrange equation set based on variational calculus in HOL light ⋮ TacticToe: learning to prove with tactics ⋮ Machine learning guidance for connection tableaux ⋮ On the Key Dependent Message Security of the Fujisaki-Okamoto Constructions ⋮ Verification of dynamic bisimulation theorems in Coq ⋮ Formal Dependability Modeling and Analysis: A Survey ⋮ The verified CakeML compiler backend ⋮ Validating QBF Validity in HOL4 ⋮ A Verified Runtime for a Verified Theorem Prover ⋮ \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic ⋮ GRUNGE: a grand unified ATP challenge ⋮ HOL ⋮ HOL Zero’s Solutions for Pollack-Inconsistency ⋮ Towards the Formal Reliability Analysis of Oil and Gas Pipelines ⋮ Matching Concepts across HOL Libraries ⋮ A String of Pearls: Proofs of Fermat's Little Theorem ⋮ Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC ⋮ The 10th IJCAR automated theorem proving system competition – CASC-J10 ⋮ On the formalization of gamma function in HOL

Uses Software

Cites Work