
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 higherorder logic, intended as a clean and simplified version...

ETPS
 Referenced in 150 articles
[sw06302]
 automated theoremprover for firstorder logic and type theory. The latter ... prove theorems of first and higherorder logic interactively, automatically, or in a mixture ... proofs, and solving unification problems in higherorder logic. It has a formula editor which...

CASL
 Referenced in 167 articles
[sw02235]
 various sublanguages. It has extensions to higherorder, statebased, concurrent, and other languages...

LCF
 Referenced in 155 articles
[sw08360]
 proof assistant for higher order logic originally developed for reasoning about hardware.2 The multifaceted...

Sledgehammer
 Referenced in 106 articles
[sw07047]
 tool that harnesses external firstorder automatic theorem provers (ATPs) to discharge interactive proof obligations ... Satallax, the two most prominent higherorder ATPs, improving its performance on higherorder problems...

PROST
 Referenced in 142 articles
[sw12822]
 NavierStokes 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, higherorder functions, recursion, and the selfhosting compiler...

LEGO
 Referenced in 106 articles
[sw09685]
 that of informal mathematics. The higherorder 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 theoremprover for firstorder logic and type theory. The latter ... prove theorems of first and higherorder logic interactively, automatically, or in a mixture ... proofs, and solving unification problems in higherorder logic. It has a formula editor which...

GHC
 Referenced in 87 articles
[sw06691]
 Glasgow Haskell Compiler inliner. Higherorder languages such as Haskell encourage the programmer to build...

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

LEOII
 Referenced in 44 articles
[sw00512]
 standalone, resolutionbased higherorder theorem prover designed for fruitful cooperation with specialist provers ... natural fragments of higherorder logic. At present LEOII can cooperate with TPTP compliant ... firstorder automated theorem provers such as E, SPASS, Gandalf and Vampire. World Champion ... division (automation of higherorder logic) at CASCJ5. At CASC...

Pict
 Referenced in 70 articles
[sw08929]
 data structures, protocols for returning results, higherorder programming, selective communication, and concurrent objects...

Coq/SSReflect
 Referenced in 60 articles
[sw09360]
 Colour Theorem and which leverages the higherorder nature of Coq’s underlying logic...

Satallax
 Referenced in 41 articles
[sw06849]
 automated theorem prover for higherorder logic. The particular form of higherorder 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 SATbased firstorder relational model finder. Nitpick supports unbounded quantification ... counterexamples than other model finders for higherorder logic, without restrictions on the form...

Ynot
 Referenced in 34 articles
[sw12334]
 supports writing, reasoning about, and extracting higherorder, dependentlytyped programs with sideeffects ... abstraction mechanisms of Coq to build higherlevel reasoning mechanisms which in turn ... finite maps, including support for a higherorder (effectful) iterator. The implementations range from simple...