HOL Light
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Efficiently checking propositional refutations in HOL theorem provers
- Operating system verification---an overview
- Data compression for proof replay
- A Skeptic's approach to combining HOL and Maple
- ACETAF
- Apron
- ACL2
- BIGEBRA
- Coq
- HOL-Boogie
- Isabelle
- LEO-II
- MetiTarski
- Nitpick
- PGB
- Proviola
- ARQMath
- Theorema
- TPS
- ML
- Prosper
- Isabelle/HOL
- Isabelle/Isar
- IsaPlanner
- CAS/PI
- LINK
- MPTP
- MPTP 0.2
- VLISP
- VAMPIRE
- HOL-Z
- THF0
- PVS
- CoqEAL
- MathWebSearch
- gensim
- Algolib
- TPTP
- Formal analysis of continuous-time systems using Fourier transform
- Aligning concepts across proof assistant libraries
- Why3
- Metis
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
- Hammer for Coq: automation for dependent type theory
- Isar
- SPASS+T
- MetaPRL
- MoMM
- Mizar
- FoCaLiZe and Dedukti to the rescue for proof interoperability
- Formalizing basic quaternionic analysis
- Proof certificates in PVS
- Making PVS accessible to generic services by interpretation in a universal format
- Gauge integral
- QSopt_ex
- zChaff
- Formally proving size optimality of sorting networks
- Gappa
- cvc3
- z3
- Proof General
- Isabelle/ZF
- From types to sets by local type definition in higher-order logic
- Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials
- A consistent foundation for Isabelle/HOL
- Flexary connectives in Mizar
- Incorporating quotation and evaluation into Church's type theory
- HOL
- The coinductive formulation of common knowledge
- A formalization of the LLL basis reduction algorithm
- HOL Light QE
- Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)
- Klein-Beltrami model. I
- Klein-Beltrami model. II
- Translating the IMPS theory library to MMT/OMDoc
- Biform theories: project description
- Isabelle import infrastructure for the Mizar Mathematical Library
- Exploring approximations for floating-point arithmetic using UppSAT
- Theories as types
- An abstraction-refinement framework for reasoning with large theories
- SLEEF
- Matita
- CIRC
- ETPS
- ProofPower
- OCaml
- PIDE
- Isabelle/jEdit
- HOL-Omega
- Formal verification of square root algorithms
- SCOTT
- Nuprl
- C-CoRN
- An experiment concerning mathematical proofs on computers with French undergraduate students
- Flocq
- Satallax
- Twelf
- MML
- Hets
- Sledgehammer
This page was built for software: HOL Light
