
HOL Light
 Referenced in 296 articles
[sw06580]
 interactive proof assistant for classical higherorder logic, intended as a clean and simplified version...

ETPS
 Referenced in 157 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...

Sledgehammer
 Referenced in 124 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...

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

LISP
 Referenced in 126 articles
[sw07201]
 automatic storage management, dynamic typing, conditionals, higherorder functions, recursion, and the selfhosting compiler...

LEGO
 Referenced in 107 articles
[sw09685]
 that of informal mathematics. The higherorder power of its underlying type theories...

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

TPS
 Referenced in 71 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...

LEOII
 Referenced in 51 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...

HiLog
 Referenced in 47 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...

Satallax
 Referenced in 51 articles
[sw06849]
 automated theorem prover for higherorder logic. The particular form of higherorder logic supported...

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

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

Nitpick
 Referenced in 61 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...

DiffSharp
 Referenced in 36 articles
[sw16033]
 Jacobianvector products) is applied using higherorder functions, that is, functions which take other ... meaning that you can compute exact higherorder derivatives or differentiate functions that are internally...

dcc
 Referenced in 35 articles
[sw07577]
 generation of first and higherorder tangentlinear and adjoint code. The author covers ... examples and exercises; * first and higherorder tangentlinear and adjoint modes for a limited...

Ynot
 Referenced in 35 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...

Ciao
 Referenced in 47 articles
[sw12088]
 language which supports logic, constraint, functional, higherorder, and objectoriented programming styles. Its main...

FDL3DI
 Referenced in 45 articles
[sw24948]
 Implementation Into FDL3DI. A spectrum of higherorder schemes is developed to solve the Navier...

LambdaClam
 Referenced in 24 articles
[sw19614]
 system that support proof planning over higherorder domains: System description: Proof planning in higher ... λClam system for proof planning in higherorder logic. The usefulness and feasibility of applying ... higherorder proof planning to a number of types of problem is outlined, in particular ... hardware systems. The use of a higherorder metatheory overcomes problems encountered in Clam because...