HOL Light

swMATH6580MaRDI QIDQ18672FDOQ18672

Author name not available (Why is that?)

Cited In (only showing first 100 items - show all)

• Formal Proofs for Nonlinear Optimization
• Cardinals in Isabelle/HOL
• From types to sets by local type definition in higher-order logic
• Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
• Title not available (Why is that?)
• Mechanized metatheory revisited
• Views of Pi: definition and computation
• Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics
• Real Number Calculations and Theorem Proving
• A Consistent Foundation for Isabelle/HOL
• Theorem Proving in Higher Order Logics
• Formalizing an analytic proof of the prime number theorem
• Incorporating quotation and evaluation into Church's type theory
• From Types to Sets by Local Type Definitions in Higher-Order Logic
• Formal Methods in Computer-Aided Design
• Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7--11, 2014. Proceedings
• Efficient formal verification of bounds of linear programs
• Formal analysis of continuous-time systems using Fourier transform
• A formalization of the LLL basis reduction algorithm
• Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17--21, 2017. Proceedings
• Formalization of linear space theory in the higher-order logic proving system
• Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
• Title not available (Why is that?)
• Rocket-Fast Proof Checking for SMT Solvers
• TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
• QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge
• Theory morphisms in Church's type theory with quotation and evaluation
• An Interpretation of Isabelle/HOL in HOL Light
• Checking Conservativity of Overloaded Definitions in Higher-Order Logic
• Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm
• Formalization of transform methods using HOL Light
• The coinductive formulation of common knowledge
• Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)
• Modules over monads and initial semantics
• HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism
• Automated cyclic entailment proofs in separation logic
• Klein-Beltrami model. I
• Klein-Beltrami model. II
• Biform theories: project description
• Isabelle import infrastructure for the Mizar Mathematical Library
• Exploring approximations for floating-point arithmetic using UppSAT
• An abstraction-refinement framework for reasoning with large theories
• Translating the IMPS theory library to MMT/OMDoc
• Theories as types
• Towards the Formalization of Fractional Calculus in Higher-Order Logic
• On the Formalization of Fourier Transform in Higher-order Logic
• Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-Light
• A precision- and range-independent tool for testing floating-point arithmetric I
• Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13--17, 2015, Proceedings
• Title not available (Why is that?)
• Formalizing basic quaternionic analysis
• Making PVS accessible to generic services by interpretation in a universal format
• Proof certificates in PVS
• Gauge integral
• Formal mathematics on display: a wiki for Flyspeck
• Pascal's theorem in real projective plane
• Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
• Formally proving size optimality of sorting networks
• The higher-order-logic Formath
• A consistent foundation for Isabelle/HOL
• Comprehending Isabelle/HOL’s Consistency
• On the Formal Analysis of Geometrical Optics in HOL
• Extending Sledgehammer with SMT solvers
• The future of logic: foundation-independence
• A web-based toolkit for mathematical word processing applications with semantics
• Metamath Zero: designing a theorem prover prover
• WorkflowFM: a logic-based framework for formal process specification and composition
• Towards Knowledge Management for HOL Light
• Lem: reusable engineering of real-world semantics
• Representing model theory in a type-theoretical logical framework
• Certification of bounds on expressions involving rounded operators
• A synthesis of the procedural and declarative styles of interactive theorem proving
• A Brief Overview of Mizar
• Friends with Benefits
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The Lean Theorem Prover (System Description)
• THF0 – The Core of the TPTP Language for Higher-Order Logic
• Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec
• A heuristic prover for real inequalities
• On definitions of constants and types in HOL
• The higher-order prover \textsc{Leo}-II
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• Mechanizing metatheory in a logical framework
• Steps towards Verified Implementations of HOL Light
• Automated Deduction – CADE-20
• FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
• Deciding floating-point logic with abstract conflict driven clause learning
• An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs
• Fast LCF-Style Proof Reconstruction for Z3
• Efficiently checking propositional refutations in HOL theorem provers
• On the formal analysis of Gaussian optical systems in HOL
• On the Formalization of Cardinal Points of Optical Systems
• Formal analysis of optical systems
• A Skeptic's approach to combining HOL and Maple
• TacticToe: Learning to Reason with HOL4 Tactics
• A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
• Title not available (Why is that?)

This page was built for software: HOL Light