• Charge!

  • Referenced in 8 articles [sw22731]
  • Charge! A framework for higher-order separation logic in Coq. We present a comprehensive ... shallow embedding of a higher-order separation logic for a subset of Java...
  • Leo-III

  • Referenced in 8 articles [sw18516]
  • agent-based deduction system for classical higher-order logic is developed. Leo-III 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 higher-order logic and supply explicit machine-checkable proof...
  • CFML

  • Referenced in 8 articles [sw13287]
  • pure Caml program, this tool generates a logical formula that implies any valid post-condition ... that they are expressible in standard higher-order logic, allowing to exploit them in practice...
  • Teyjus

  • Referenced in 16 articles [sw21364]
  • intuitionistic theory of higher-order hereditary Harrop formulas, a logic that significantly extends the theory...
  • Hiord

  • Referenced in 4 articles [sw07313]
  • Hiord: A type-free higher-order logic programming language with predicate abstraction A new formalism ... called Hiord, for defining type-free higher-order logic programming languages with predicate abstraction...
  • LeoPARD

  • Referenced in 6 articles [sw13554]
  • knowledge representation and reasoning tools for higher-order logic(s). It combines a sophisticated data...
  • RGITL

  • Referenced in 5 articles [sw13917]
  • interval temporal logic (ITL) and higher-order 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 higher-order power of its underlying type theories...
  • SigmaKEE

  • Referenced in 4 articles [sw15189]
  • large, comprehensive ontology stated in higher-order logic. It has co-evolved with a development...
  • FMLtoHOL

  • Referenced in 3 articles [sw21539]
  • modeled as natural fragments of classical higher-order logic (HOL). The FMLtoHOL tool exploits this...
  • Monomorphic Monad

  • Referenced in 2 articles [sw28583]
  • Effect polymorphism in higher-order logic. The notion of a monad cannot be expressed within ... higher-order 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 higher-order logic, alphabets, equational reasoning and “programs...
  • UTP2

  • Referenced in 3 articles [sw06342]
  • design goal was to support the higher-order logic, alphabets, equational reasoning and “programs...
  • AgsyHOL

  • Referenced in 3 articles [sw13302]
  • agsyHol is a theorem prover for higher-order logic. It reads problems in the TPTP...
  • HOL88

  • Referenced in 2 articles [sw19615]
  • interactive theorem proving in a higher-order logic. Its most outstanding feature is its high...
  • embed_modal

  • Referenced in 1 article [sw28304]
  • higher-order modal logic into classical higher-order logic. The procedure was implemented...
  • ModuRes

  • Referenced in 3 articles [sw13122]
  • library for modular reasoning about concurrent higher-order imperative programming languages. It is well-known ... type systems or logics for reasoning about concurrent higher-order imperative programming languages ... type systems and logics for reasoning about concurrent higher-order imperative programming languages...
  • Paraconsistency

  • Referenced in 1 article [sw28572]
  • propositional fragment of the higher-order logic. The logic is based on so-called...
  • Holophrasm

  • Referenced in 1 article [sw30124]
  • neural Automated Theorem Prover for higher-order logic. I propose a system for Automated Theorem...