• OpenTheory

  • Referenced in 17 articles [sw32625]
  • prover implementations of higher order logic, including HOL Light, HOL4 and ProofPower. It is hoped...
  • HOL-TestGen

  • Referenced in 10 articles [sw17720]
  • HOL-TestGen is a is a test case generator for specification based unit testing ... HOL-TestGen is built on top of the specfication and theorem proving environment Isabelle/HOL...
  • Leo-III

  • Referenced in 16 articles [sw18516]
  • Agent-based HOL reasoning. In the Leo-III project, a new agent-based deduction system...
  • miz3

  • Referenced in 11 articles [sw18631]
  • interface called miz3 , on top of the HOL Light interactive theorem prover. The declarative language ... tactics and formal libraries of HOL Light, and as such has ‘industrial strength’. Our approach...
  • ivreg2

  • Referenced in 15 articles [sw31884]
  • choice of kernel; Cragg’s ”heteroskedastic OLS” (HOLS) estimator; default reporting of large-sample statistics...
  • Separation Logic

  • Referenced in 8 articles [sw28549]
  • Separation Logic Framework for Imperative HOL. We provide a framework for separation-logic based correctness ... proofs of Imperative HOL programs. Our framework comes with a set of proof methods ... data-refinement techniques. As we target Imperative HOL, our programs can be translated to efficiently...
  • Isabelle/PIDE

  • Referenced in 13 articles [sw07185]
  • traditionally strong logical foundations of systems like HOL, Coq, or Isabelle have so far been...
  • TkWinHOL

  • Referenced in 8 articles [sw00968]
  • contextual rewriting and renement supported by the HOL Window Inference Library. This paper describes ... transformation step is proved automatically by the HOL system. The interface can be tailored...
  • PIDE

  • Referenced in 11 articles [sw06404]
  • HOL [5, {S}1]) with sophisticated front-end technology on the JVM platform, overcoming command...
  • GoedelGod

  • Referenced in 7 articles [sw32223]
  • fragment of classical higher-order logic (HOL); thus, the formalization is essentially a formalization ... HOL...
  • TacticToe

  • Referenced in 6 articles [sw28627]
  • translation to FOL, working directly on the HOL level. By combining tactic prediction and premise ... seconds whereas the best single HOL(y)Hammer strategy solves 32 percent in the same...
  • FMLtoHOL

  • Referenced in 4 articles [sw21539]
  • HOL based first-order modal logic provers. First-order modal logics (FMLs) can be modeled ... natural fragments of classical higher-order logic (HOL). The FMLtoHOL tool exploits this fact ... enables the application of off-the-shelf HOL provers and model finders for reasoning within ... TPTP thf0-syntax for HOL. It currently supports logics...
  • HOL2P

  • Referenced in 4 articles [sw21180]
  • HOL2P that extends classical higher order logic (HOL) with type operator variables and universal types ... applied at the level of polymorphic HOL functions. The parameterisation of terms with type operators ... HOL2P has been implemented on top of HOL-Light. Type inference is semi-automatic...
  • HOL Light QE

  • Referenced in 3 articles [sw28656]
  • HOL Light QE. We are interested in algorithms that manipulate mathematical expressions in mathematically meaningful ... Lisp programming language. Since the HOL logic is also a version of Church’s type ... decided to add quotation and evaluation to HOL Light to demonstrate the implementability of CTTqe ... proof assistant. The resulting system is called HOL Light QE. Here we document the design...
  • HOL-UNITY

  • Referenced in 3 articles [sw28702]
  • HOL-UNITY verification system. The HOL-UNITY verification system consists of a collection of tools ... tools interface the theorem prover HOL for proving the properties of UNITY programs. In this ... HOL-UNITY supports mechanised proving of correctness for parallel programs...
  • Tactician

  • Referenced in 6 articles [sw17591]
  • tool for helping you maintain and/or understand HOL Light proof scripts. Its main function...
  • lcpSim

  • Referenced in 6 articles [sw18603]
  • service disciplines, such as FIFO, LIPO, PPS, HOL, Preemptive Priorities (Resume, Repeat), Transfer, Polling, Nearest...
  • Monomorphic Monad

  • Referenced in 3 articles [sw28583]
  • cannot be expressed within higher-order logic (HOL) due to type system restrictions. We show ... type, this notion can be formalised in HOL. Based on this idea, we develop ... abstract over the concrete monad in HOL definitions and thus use the same definition...
  • IMP++

  • Referenced in 4 articles [sw01439]
  • encoding of object-oriented data models in HOL. With an application...
  • AgsyHOL

  • Referenced in 4 articles [sw13302]
  • applied to a proof checker for a HOL proof term language. The term language...