• HOL

  • Referenced in 460 articles [sw05492]
  • Higher Order Logic (HOL) is a programming environment in which theorems can be proved...
  • HOL Light

  • Referenced in 274 articles [sw06580]
  • interactive proof assistant for classical higher-order logic, intended as a clean and simplified version...
  • ETPS

  • Referenced in 150 articles [sw06302]
  • automated theorem-prover for first-order logic and type theory. The latter ... prove theorems of first- and higher-order logic interactively, automatically, or in a mixture ... proofs, and solving unification problems in higher-order logic. It has a formula editor which...
  • CASL

  • Referenced in 167 articles [sw02235]
  • various sublanguages. It has extensions to higher-order, state-based, concurrent, and other languages...
  • LCF

  • Referenced in 155 articles [sw08360]
  • proof assistant for higher order logic originally developed for reasoning about hardware.2 The multi-faceted...
  • Sledgehammer

  • Referenced in 106 articles [sw07047]
  • tool that harnesses external first-order automatic theorem provers (ATPs) to discharge interactive proof obligations ... Satallax, the two most prominent higher-order ATPs, improving its performance on higher-order problems...
  • PROST

  • Referenced in 142 articles [sw12822]
  • Navier-Stokes solver, and a higher order interface advection scheme. The curvature to the interface...
  • LISP

  • Referenced in 123 articles [sw07201]
  • automatic storage management, dynamic typing, conditionals, higher-order functions, recursion, and the self-hosting compiler...
  • LEGO

  • Referenced in 106 articles [sw09685]
  • that of informal mathematics. The higher-order power of its underlying type theories...
  • ICALAB

  • Referenced in 103 articles [sw15047]
  • independent component analysis) employing HOS (higher order statistics), BSS (blind source separation) employing SOS (second...
  • TPS

  • Referenced in 69 articles [sw00973]
  • automated theorem-prover for first-order logic and type theory. The latter ... prove theorems of first- and higher-order logic interactively, automatically, or in a mixture ... proofs, and solving unification problems in higher-order logic. It has a formula editor which...
  • GHC

  • Referenced in 87 articles [sw06691]
  • Glasgow Haskell Compiler inliner. Higher-order languages such as Haskell encourage the programmer to build...
  • HiLog

  • Referenced in 45 articles [sw01580]
  • HiLog: A foundation for higher-order logic programming. We describe a novel logic, called HiLog ... traditional predicate logic. HiLog has a higher-order syntax and allows arbitrary terms to appear ... predicate calculus. But its semantics is first-order and admits a sound and complete proof ... HiLog are discussed, including DCG grammars, higher-order and modular logic programming, and deductive databases...
  • LEO-II

  • Referenced in 44 articles [sw00512]
  • standalone, resolution-based higher-order theorem prover designed for fruitful cooperation with specialist provers ... natural fragments of higher-order logic. At present LEO-II can cooperate with TPTP compliant ... first-order automated theorem provers such as E, SPASS, Gandalf and Vampire. World Champion ... division (automation of higher-order logic) at CASC-J5. At CASC...
  • Pict

  • Referenced in 70 articles [sw08929]
  • data structures, protocols for returning results, higher-order programming, selective communication, and concurrent objects...
  • Coq/SSReflect

  • Referenced in 60 articles [sw09360]
  • Colour Theorem and which leverages the higher-order nature of Coq’s underlying logic...
  • Satallax

  • Referenced in 41 articles [sw06849]
  • automated theorem prover for higher-order logic. The particular form of higher-order logic supported...
  • ProofPower

  • Referenced in 51 articles [sw06339]
  • tool based on an implementation of Higher Order Logic (HOL), following the LCF paradigm...
  • Nitpick

  • Referenced in 50 articles [sw00622]
  • builds on Kodkod, a SAT-based first-order relational model finder. Nitpick supports unbounded quantification ... counterexamples than other model finders for higher-order logic, without restrictions on the form...
  • Ynot

  • Referenced in 34 articles [sw12334]
  • supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects ... abstraction mechanisms of Coq to build higher-level reasoning mechanisms which in turn ... finite maps, including support for a higher-order (effectful) iterator. The implementations range from simple...