
Charge!
 Referenced in 8 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...

LeoIII
 Referenced in 8 articles
[sw18516]
 agentbased deduction system for classical higherorder logic is developed. LeoIII combines...

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...

LEGO
 Referenced in 106 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...

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...

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...

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

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...

Paraconsistency
 Referenced in 1 article
[sw28572]
 propositional fragment of the higherorder logic. The logic is based on socalled...

Holophrasm
 Referenced in 1 article
[sw30124]
 neural Automated Theorem Prover for higherorder logic. I propose a system for Automated Theorem...