The following pages link to A Brief Overview of HOL4 (Q3543646):
Displaying 25 items.
- 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)
- 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)
- Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
- Psi-calculi in Isabelle (Q5890661) (← links)
- Deductive Binary Code Verification Against Source-Code-Level Specifications (Q6487259) (← links)
- Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction (Q6487292) (← links)
- Hammering Floating-Point Arithmetic (Q6496632) (← links)
- Learning Proof Transformations and Its Applications in Interactive Theorem Proving (Q6496633) (← links)
