HOL Light: An Overview
From MaRDI portal
Publication:3183517
DOI10.1007/978-3-642-03359-9_4zbMath1252.68255OpenAlexW1600435877MaRDI QIDQ3183517
No author found.
Publication date: 20 October 2009
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-03359-9_4
Related Items
Formal verification of stability and chaos in periodic optical systems, A FORMAL PROOF OF THE KEPLER CONJECTURE, Theory morphisms in Church's type theory with quotation and evaluation, 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, JEFL: joint embedding of formal proof libraries, An experiment concerning mathematical proofs on computers with French undergraduate students, The Imandra Automated Reasoning System (System Description), The Lean Theorem Prover (System Description), On the formal analysis of Gaussian optical systems in HOL, Aligning concepts across proof assistant libraries, Floating-point arithmetic on the test bench. How are verified numerical solutions calculated?, Interacting with Modal Logics in the Coq Proof Assistant, Hammer for Coq: automation for dependent type theory, Extensional higher-order paramodulation in Leo-III, Proof-Producing Reflection for HOL, Pattern Matches in HOL:, A formalised theorem in the partition calculus, Formalization of functional variation in HOL Light, 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, A condensed semantics for qualitative spatial reasoning about oriented straight line segments, Formalization of real analysis: a survey of proof assistants and libraries, Friends with Benefits, Comprehending Isabelle/HOL’s Consistency, Formal analysis of optical systems, A verified proof checker for higher-order logic, Incorporating quotation and evaluation into Church's type theory, 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, Automated Cyclic Entailment Proofs in Separation Logic, Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions, Distilling the requirements of Gödel's incompleteness theorems with a proof assistant, Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics, A Verified Runtime for a Verified Theorem Prover, Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism, Mechanised Computability Theory, Verified interactive computation of definite integrals, HOL Zero’s Solutions for Pollack-Inconsistency, Mechanized metatheory revisited, Formalization of geometric algebra in HOL Light, Formalization of Complex Vectors in Higher-Order Logic, Matching Concepts across HOL Libraries, Proof Auditing Formalised Mathematics, Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Some new results on decidability for elementary algebra and geometry
- A type-theoretical alternative to ISWIM, CUCH, OWHY
- Edinburgh LCF. A mechanized logic of computation
- Formalizing an analytic proof of the prime number theorem
- Verifying Nonlinear Real Formulas Via Sums of Squares
- Axiom of Choice and Complementation
- The Jordan Curve Theorem, Formally and Informally
- Mechanical Theorem-Proving by Model Elimination
- A formulation of the simple theory of types
- Formal Methods for Hardware Verification
