HOL Light: An Overview
From MaRDI portal
Recommendations
Cites work
- A formulation of the simple theory of types
- A type-theoretical alternative to ISWIM, CUCH, OWHY
- Axiom of Choice and Complementation
- Edinburgh LCF. A mechanized logic of computation
- Formal Methods for Hardware Verification
- Formalizing an analytic proof of the prime number theorem
- scientific article; zbMATH DE number 3959364 (Why is no real title available?)
- scientific article; zbMATH DE number 3999882 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- Mechanical Theorem-Proving by Model Elimination
- Some new results on decidability for elementary algebra and geometry
- The Jordan Curve Theorem, Formally and Informally
- Verifying Nonlinear Real Formulas Via Sums of Squares
Cited in
(82)- Aligning concepts across proof assistant libraries
- Hammer for Coq: automation for dependent type theory
- Incorporating quotation and evaluation into Church's type theory
- HOL Light QE
- An experiment concerning mathematical proofs on computers with French undergraduate students
- A verified proof checker for higher-order logic
- HOL(y)Hammer: online ATP service for HOL Light
- Coquelicot: a user-friendly library of real analysis for Coq
- 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
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- Verified interactive computation of definite integrals
- From LCF to Isabelle/HOL
- Mechanized metatheory revisited
- Formalization of geometric algebra in HOL Light
- Formal verification of stability and chaos in periodic optical systems
- Theory morphisms in Church's type theory with quotation and evaluation
- Formalization of functional variation in HOL Light
- Extensional higher-order paramodulation in Leo-III
- scientific article; zbMATH DE number 1670733 (Why is no real title available?)
- Incorporating quotation and evaluation into Church's type theory: syntax and semantics
- HOL Zero's solutions for Pollack-inconsistency
- Automated reasoning service for HOL Light
- Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- The higher-order prover \textsc{Leo}-II
- On definitions of constants and types in HOL
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- Proof-producing reflection for HOL. With an application to model polymorphism
- Improved tool support for machine-code decompilation in HOL4
- Pattern matches in HOL: a new representation and improved code generation
- Formalization of real analysis: a survey of proof assistants and libraries
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Comprehending Isabelle/HOL’s Consistency
- A verified runtime for a verified theorem prover
- Verified efficient enumeration of plane graphs modulo isomorphism
- Mechanised computability theory
- On the formal analysis of Gaussian optical systems in HOL
- Interacting with Modal Logics in the Coq Proof Assistant
- Floating-point arithmetic on the test bench. How are verified numerical solutions calculated?
- Enabling symbolic and numerical computations in HOL Light
- The Lean theorem prover (system description)
- A Brief Overview of HOL4
- Towards Self-verification of HOL Light
- An Interpretation of Isabelle/HOL in HOL Light
- A condensed semantics for qualitative spatial reasoning about oriented straight line segments
- Formal analysis of optical systems
- An Isabelle-like procedural mode for HOL Light
- Stateless HOL
- The Imandra Automated Reasoning System (System Description)
- Proof auditing formalised mathematics
- Conversion of HOL Light proofs into Metamath
- Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
- Automated cyclic entailment proofs in separation logic
- Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
- A formal proof of the Kepler conjecture
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- Formalization of complex vectors in higher-order logic
- Matching concepts across HOL libraries
- Towards Knowledge Management for HOL Light
- A formalised theorem in the partition calculus
- What is the point of computers? A question for pure mathematicians
- Formalization of the inverse kinematics of three-fingered dexterous hand
- Combining higher-order logic with set theory formalizations
- Equivalence checking for orthocomplemented bisemilattices in log-linear time
- Formula normalizations in verification
- Linear resources in Isabelle/HOL
- On the Erdős-Tuza-Valtr conjecture
- Iterative monomorphisation
- Mechanized HOL reasoning in set theory
- A formal proof of R(4,5)=25
- Interoperability of proof systems with SC-TPTP
- Notes on Gödel's and Scott's variants of the ontological argument
- Semantical investigations on non-classical logics with recovery operators: negation
- Fast, verified computation for HOL ITPs
- A mechanised semantics for HOL with ad-hoc overloading
- Experiments with choice in dependently-typed higher-order logic
- Translating HOL-Light proofs to Coq
- Experiments on infinite model finding in SMT solving
- Formalizing colimits in \(\mathcal{C}\)at
- JEFL: joint embedding of formal proof libraries
This page was built for publication: HOL Light: An Overview
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3183517)
