
Charge!
 Referenced in 9 articles
[sw22731]
 Charge! A framework for higherorder separation logic in Coq. We present a comprehensive ... shallow embedding of a higherorder separation logic for a subset of Java...

AUTO2
 Referenced in 6 articles
[sw17595]
 saturationbased heuristic prover for higherorder logic. We introduce a new theorem prover ... classical higherorder logic named auto2. The prover is designed to make use of human...

VeriML
 Referenced in 8 articles
[sw13522]
 VeriML: typed computation of logical terms inside a language with effects. Modern proof assistants such ... because they support formal reasoning in higherorder logic and supply explicit machinecheckable proof...

CFML
 Referenced in 8 articles
[sw13287]
 pure Caml program, this tool generates a logical formula that implies any valid postcondition ... that they are expressible in standard higherorder logic, allowing to exploit them in practice...

Teyjus
 Referenced in 16 articles
[sw21364]
 intuitionistic theory of higherorder hereditary Harrop formulas, a logic that significantly extends the theory...

Hiord
 Referenced in 4 articles
[sw07313]
 Hiord: A typefree higherorder logic programming language with predicate abstraction A new formalism ... called Hiord, for defining typefree higherorder logic programming languages with predicate abstraction...

LeoPARD
 Referenced in 6 articles
[sw13554]
 knowledge representation and reasoning tools for higherorder logic(s). It combines a sophisticated data...

RGITL
 Referenced in 5 articles
[sw13917]
 interval temporal logic (ITL) and higherorder logic. It extends ITL with explicit interleaved programs...

GoedelGod
 Referenced in 5 articles
[sw32223]
 modeled as a fragment of classical higherorder logic (HOL); thus, the formalization is essentially...

LEGO
 Referenced in 107 articles
[sw09685]
 implements various related type systems  the Edinburgh Logical Framework (LF), the Calculus of Constructions ... that of informal mathematics. The higherorder power of its underlying type theories...

SigmaKEE
 Referenced in 4 articles
[sw15189]
 large, comprehensive ontology stated in higherorder logic. It has coevolved with a development...

AgsyHOL
 Referenced in 4 articles
[sw13302]
 agsyHol is a theorem prover for higherorder logic. It reads problems in the TPTP...

FMLtoHOL
 Referenced in 3 articles
[sw21539]
 modeled as natural fragments of classical higherorder logic (HOL). The FMLtoHOL tool exploits this...

Monomorphic Monad
 Referenced in 2 articles
[sw28583]
 Effect polymorphism in higherorder logic. The notion of a monad cannot be expressed within ... higherorder logic (HOL) due to type system restrictions. We show that if a monad...

Zipperposition
 Referenced in 3 articles
[sw32251]
 theorem prover in OCaml for typed higherorder logic with equality, datatypes and arithmetic, based...

Saoithin
 Referenced in 3 articles
[sw06341]
 design goal was to support the higherorder logic, alphabets, equational reasoning and “programs...

UTP2
 Referenced in 3 articles
[sw06342]
 design goal was to support the higherorder logic, alphabets, equational reasoning and “programs...

HOL88
 Referenced in 2 articles
[sw19615]
 interactive theorem proving in a higherorder logic. Its most outstanding feature is its high...

embed_modal
 Referenced in 1 article
[sw28304]
 higherorder modal logic into classical higherorder logic. The procedure was implemented...

ModuRes
 Referenced in 3 articles
[sw13122]
 library for modular reasoning about concurrent higherorder imperative programming languages. It is wellknown ... type systems or logics for reasoning about concurrent higherorder imperative programming languages ... type systems and logics for reasoning about concurrent higherorder imperative programming languages...