A Brief Overview of HOL4

From MaRDI portal
Revision as of 00:57, 5 February 2024 by Import240129110113 (talk | contribs) (Created automatically from import240129110113)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Publication:3543646

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

Konrad Slind, Michael Norrish

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




Related Items (61)

The reflective Milawa theorem prover is sound (down to the machine code that runs it)On definitions of constants and types in HOLSelf-formalisation of higher-order logic. Semantics, soundness, and a verified implementationAutomatic Proof and Disproof in Isabelle/HOLFormalization of linear space theory in the higher-order logic proving systemThe role of entropy in guiding a connection proverAUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine CodeAligning concepts across proof assistant librariesFormalization of reliability block diagrams in higher-order logicProof producing synthesis of arithmetic and cryptographic hardwareComputer assisted reasoning. A Festschrift for Michael J. C. GordonHammer for Coq: automation for dependent type theoryFormally verified algorithms for upper-bounding state space diametersExtensional higher-order paramodulation in Leo-IIIA mechanisation of some context-free language theory in HOL4Verified Over-Approximation of the Diameter of Propositionally Factored Transition SystemsProof-Producing Reflection for HOLPattern Matches in HOL:A formalized general theory of syntax with bindingsFormalization of functional variation in HOL LightTactics for hierarchical proofUnnamed ItemTheoretical and practical approaches to the denotational semantics for MDESL based on UTPQuantified multimodal logics in simple type theoryParameterized synthesis for fragments of first-order logic over data wordsFunction extractionMonotonicity inference for higher-order formulasAnalytic tableaux for higher-order logic with choiceFormal reasoning under cached address translationUnnamed ItemPsi-calculi in IsabelleUnique solutions of contractions, CCS, and their HOL formalisationFriends with BenefitsThe CADE-27 Automated theorem proving System Competition – CASC-27A Verified Compositional Algorithm for AI Planning\texttt{cake\_lpr}: verified propagation redundancy checking in CakeMLA verified proof checker for higher-order logicHighly Automated Formal Proofs over Memory Usage of Assembly CodeThe right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4Transforming Programs into Recursive FunctionsMonotonicity Inference for Higher-Order FormulasFrom LCF to Isabelle/HOLFormalization of Euler-Lagrange equation set based on variational calculus in HOL lightTacticToe: learning to prove with tacticsMachine learning guidance for connection tableauxOn the Key Dependent Message Security of the Fujisaki-Okamoto ConstructionsVerification of dynamic bisimulation theorems in CoqFormal Dependability Modeling and Analysis: A SurveyThe verified CakeML compiler backendValidating QBF Validity in HOL4A Verified Runtime for a Verified Theorem Prover\(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logicGRUNGE: a grand unified ATP challengeHOLHOL Zero’s Solutions for Pollack-InconsistencyTowards the Formal Reliability Analysis of Oil and Gas PipelinesMatching Concepts across HOL LibrariesA String of Pearls: Proofs of Fermat's Little TheoremUnderstanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoCThe 10th IJCAR automated theorem proving system competition – CASC-J10On the formalization of gamma function in HOL


Uses Software


Cites Work


This page was built for publication: A Brief Overview of HOL4