The following pages link to HOL Light: An Overview (Q3183517):
Displaying 50 items.
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- The higher-order prover \textsc{Leo}-II (Q287283) (← 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)
- On the formal analysis of Gaussian optical systems in HOL (Q315313) (← links)
- Floating-point arithmetic on the test bench. How are verified numerical solutions calculated? (Q335016) (← links)
- A condensed semantics for qualitative spatial reasoning about oriented straight line segments (Q420800) (← links)
- Formal analysis of optical systems (Q475384) (← links)
- JEFL: joint embedding of formal proof libraries (Q831932) (← links)
- Aligning concepts across proof assistant libraries (Q1640642) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Incorporating quotation and evaluation into Church's type theory (Q1753993) (← links)
- An experiment concerning mathematical proofs on computers with French undergraduate students (Q1884267) (← links)
- A verified proof checker for higher-order logic (Q1987736) (← links)
- Coquelicot: a user-friendly library of real analysis for Coq (Q2018661) (← 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)
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant (Q2051568) (← links)
- Verified interactive computation of definite integrals (Q2055881) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Formalization of geometric algebra in HOL Light (Q2323452) (← links)
- Formal verification of stability and chaos in periodic optical systems (Q2361358) (← links)
- Theory morphisms in Church's type theory with quotation and evaluation (Q2364672) (← links)
- Formalization of functional variation in HOL Light (Q2423767) (← links)
- Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
- Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics (Q2817296) (← links)
- HOL Zero’s Solutions for Pollack-Inconsistency (Q2829240) (← links)
- Proof-Producing Reflection for HOL (Q2945631) (← links)
- Pattern Matches in HOL: (Q2945657) (← links)
- Formalization of real analysis: a survey of proof assistants and libraries (Q2973239) (← links)
- Friends with Benefits (Q2988636) (← links)
- Comprehending Isabelle/HOL’s Consistency (Q2988665) (← links)
- A Verified Runtime for a Verified Theorem Prover (Q3088011) (← links)
- Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism (Q3088012) (← links)
- Mechanised Computability Theory (Q3088013) (← links)
- Interacting with Modal Logics in the Coq Proof Assistant (Q3194730) (← links)
- The Lean Theorem Prover (System Description) (Q3454108) (← links)
- The Imandra Automated Reasoning System (System Description) (Q5049029) (← links)
- Proof Auditing Formalised Mathematics (Q5195266) (← links)
- Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC (Q5195279) (← links)
- Automated Cyclic Entailment Proofs in Separation Logic (Q5200020) (← links)
- Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions (Q5206960) (← links)
- A FORMAL PROOF OF THE KEPLER CONJECTURE (Q5280247) (← links)
- Formalization of Complex Vectors in Higher-Order Logic (Q5495918) (← links)
- Matching Concepts across HOL Libraries (Q5495929) (← links)
- A formalised theorem in the partition calculus (Q6073894) (← links)
- What is the point of computers? A question for pure mathematicians (Q6118162) (← links)
- Formalization of the inverse kinematics of three-fingered dexterous hand (Q6156933) (← links)
- Combining higher-order logic with set theory formalizations (Q6161232) (← links)
