The following pages link to A Brief Overview of HOL4 (Q3543646):
Displaying 50 items.
- HOL (Q17631) (← links)
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- On definitions of constants and types in HOL (Q287358) (← links)
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (Q287361) (← links)
- Formalization of reliability block diagrams in higher-order logic (Q334147) (← links)
- A mechanisation of some context-free language theory in HOL4 (Q386032) (← links)
- Function extraction (Q436372) (← links)
- Monotonicity inference for higher-order formulas (Q438558) (← links)
- Analytic tableaux for higher-order logic with choice (Q438561) (← links)
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4 (Q540690) (← links)
- Tactics for hierarchical proof (Q626933) (← links)
- Aligning concepts across proof assistant libraries (Q1640642) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Formally verified algorithms for upper-bounding state space diameters (Q1663245) (← links)
- A formalized general theory of syntax with bindings (Q1687739) (← links)
- Quantified multimodal logics in simple type theory (Q1945702) (← links)
- A verified proof checker for higher-order logic (Q1987736) (← links)
- Formalization of Euler-Lagrange equation set based on variational calculus in HOL light (Q2031406) (← links)
- TacticToe: learning to prove with tactics (Q2031416) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- Verification of dynamic bisimulation theorems in Coq (Q2035655) (← links)
- The role of entropy in guiding a connection prover (Q2142077) (← links)
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP (Q2198135) (← links)
- Parameterized synthesis for fragments of first-order logic over data words (Q2200816) (← links)
- Formal reasoning under cached address translation (Q2209539) (← links)
- Unique solutions of contractions, CCS, and their HOL formalisation (Q2216120) (← links)
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML (Q2233509) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic (Q2305408) (← links)
- GRUNGE: a grand unified ATP challenge (Q2305410) (← links)
- On the formalization of gamma function in HOL (Q2352499) (← links)
- Formalization of linear space theory in the higher-order logic proving system (Q2375439) (← links)
- Formalization of functional variation in HOL Light (Q2423767) (← links)
- Proof producing synthesis of arithmetic and cryptographic hardware (Q2642982) (← links)
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon (Q2655321) (← links)
- Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
- On the Key Dependent Message Security of the Fujisaki-Okamoto Constructions (Q2798773) (← links)
- Formal Dependability Modeling and Analysis: A Survey (Q2817299) (← links)
- HOL Zero’s Solutions for Pollack-Inconsistency (Q2829240) (← links)
- Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems (Q2945619) (← links)
- Proof-Producing Reflection for HOL (Q2945631) (← links)
- Pattern Matches in HOL: (Q2945657) (← links)
- Friends with Benefits (Q2988636) (← links)
- Validating QBF Validity in HOL4 (Q3088005) (← links)
- A Verified Runtime for a Verified Theorem Prover (Q3088011) (← links)
- Automatic Proof and Disproof in Isabelle/HOL (Q3172879) (← links)
- AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code (Q3179279) (← links)
- (Q3384919) (← links)
- The verified CakeML compiler backend (Q4972072) (← links)
- The 10th IJCAR automated theorem proving system competition – CASC-J10 (Q5019796) (← links)
