A Brief Overview of HOL4
From MaRDI portal
Recommendations
Cites work
- A formulation of the simple theory of types
- A Sound Semantics for OCaml light
- A Thread of HOL Development
- Compilation as Rewriting in Higher Order Logic
- Hoare Logic for Realistically Modelled Machine Code
- scientific article; zbMATH DE number 1670733 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- Ott, effective tool support for the working semanticist
- Proof producing synthesis of arithmetic and cryptographic hardware
Cited in
(83)- Aligning concepts across proof assistant libraries
- Hammer for Coq: automation for dependent type theory
- Formally verified algorithms for upper-bounding state space diameters
- A formalized general theory of syntax with bindings
- HOL
- Quantified multimodal logics in simple type theory
- A verified proof checker for higher-order logic
- 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
- Verification of dynamic bisimulation theorems in Coq
- The role of entropy in guiding a connection prover
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
- Parameterized synthesis for fragments of first-order logic over data words
- Formal reasoning under cached address translation
- Unique solutions of contractions, CCS, and their HOL formalisation
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
- From LCF to Isabelle/HOL
- \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic
- GRUNGE: a grand unified ATP challenge
- On the formalization of gamma function in HOL
- Formalization of linear space theory in the higher-order logic proving system
- Formalization of functional variation in HOL Light
- Proof producing synthesis of arithmetic and cryptographic hardware
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
- Extensional higher-order paramodulation in Leo-III
- On the key dependent message security of the Fujisaki-Okamoto constructions
- Formal dependability modeling and analysis: a survey
- HOL Zero's solutions for Pollack-inconsistency
- 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
- Verified over-approximation of the diameter of propositionally factored transition systems
- Proof-producing reflection for HOL. With an application to model polymorphism
- Pattern matches in HOL: a new representation and improved code generation
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Validating QBF Validity in HOL4
- A verified runtime for a verified theorem prover
- Automatic proof and disproof in Isabelle/HOL
- AUSPICE-R: automatic safety-property proofs for realistic features in machine code
- HOL Light: An Overview
- Formalization of reliability block diagrams in higher-order logic
- Unique solutions of contractions, CCS, and their HOL formalisation
- A Brief Overview of PVS
- A mechanisation of some context-free language theory in HOL4
- A Thread of HOL Development
- Function extraction
- Monotonicity inference for higher-order formulas
- Analytic tableaux for higher-order logic with choice
- The verified CakeML compiler backend
- The 10th IJCAR automated theorem proving system competition -- CASC-J10
- The CADE-27 automated theorem proving system competition -- CASC-27
- Highly automated formal proofs over memory usage of assembly code
- Transforming programs into recursive functions
- 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
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
- Towards the formal reliability analysis of oil and gas pipelines
- Matching concepts across HOL libraries
- Types for Proofs and Programs
- Monotonicity inference for higher-order formulas
- A Verified Compositional Algorithm for AI Planning
- scientific article; zbMATH DE number 7649970 (Why is no real title available?)
- Psi-calculi in Isabelle
- Tactics for hierarchical proof
- Deductive binary code verification against source-code-level specifications
- Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
- Hammering Floating-Point Arithmetic
- Learning Proof Transformations and Its Applications in Interactive Theorem Proving
- Iterative monomorphisation
- A generalised union of rely-guarantee and separation logic using permission algebras
- Mechanized HOL reasoning in set theory
- A formal proof of R(4,5)=25
- Duper: a proof-producing superposition theorem prover for dependent type theory
- Candle: a verified implementation of HOL Light (extended version)
- Machine learning for quantifier selection in cvc5
- Notes on Gödel's and Scott's variants of the ontological argument
- Fast, verified computation for HOL ITPs
- Deep reinforcement learning for synthesizing functions in higher-order logic
- Certified MaxSAT preprocessing
- A verified cost model for call-by-push-value
- GOL in GOL in HOL: verified circuits in Conway's game of life
This page was built for publication: A Brief Overview of HOL4
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3543646)
