• HOL Light

• Referenced in 222 articles [sw06580]
• interactive proof assistant for classical higher-order logic, intended as a clean and simplified version...

• ETPS

• Referenced in 142 articles [sw06302]
• automated theorem-prover for first-order logic and type theory. The latter ... prove theorems of first- and higher-order logic interactively, automatically, or in a mixture ... proofs, and solving unification problems in higher-order logic. It has a formula editor which...

• TPS

• Referenced in 66 articles [sw00973]
• automated theorem-prover for first-order logic and type theory. The latter ... prove theorems of first- and higher-order logic interactively, automatically, or in a mixture ... proofs, and solving unification problems in higher-order logic. It has a formula editor which...

• HiLog

• Referenced in 42 articles [sw01580]
• HiLog: A foundation for higher-order logic programming. We describe a novel logic, called HiLog ... than does traditional predicate logic. HiLog has a higher-order syntax and allows arbitrary terms ... discussed, including DCG grammars, higher-order and modular logic programming, and deductive databases...

• LEO-II

• Referenced in 37 articles [sw00512]
• specialist provers for natural fragments of higher-order logic. At present LEO-II can cooperate ... division (automation of higher-order logic) at CASC-J5. At CASC...

• Satallax

• Referenced in 31 articles [sw06849]
• automated theorem prover for higher-order logic. The particular form of higher-order logic supported...

• Nitpick

• Referenced in 35 articles [sw00622]
• counterexamples than other model finders for higher-order logic, without restrictions on the form...

• Lambda-Clam

• Referenced in 22 articles [sw19614]
• domains: System description: Proof planning in higher-order logic with λClam. This system description outlines ... λClam system for proof planning in higher-order logic. The usefulness and feasibility of applying...

• OMEGA

• Referenced in 25 articles [sw19623]
• Ωmega: A theorem prover for higher-order logic based on proof planning...

• HOL-OCL

• Referenced in 21 articles [sw05734]
• Object Constraint Language (OCL) in higher-order logic, we explore several key issues...

• Ciao

• Referenced in 41 articles [sw12088]
• purpose programming language which supports logic, constraint, functional, higher-order, and object-oriented programming styles...

• CCSL

• Referenced in 20 articles [sw03357]
• CCSL compiler translates CCSL specifications into higher-order logic either...

• HasCasl

• Referenced in 14 articles [sw00399]
• expressive standard language for higher-order logic. Distinctive features of HasCasl include partial higher-order ... functions, higher-order subtyping, shallow polymorphism, and an extensive type-class mechanism. Moreover, HasCasl provides ... effects, including a monad-based generic Hoare logic...

• Transfer

• Referenced in 16 articles [sw21009]
• ubiquitous in formal reasoning with higher-order logic. Typically, users want to build a library...

• Lifting

• Referenced in 16 articles [sw21010]
• ubiquitous in formal reasoning with higher-order logic. Typically, users want to build a library...

• Coq/SSReflect

• Referenced in 48 articles [sw09360]
• which leverages the higher-order nature of Coq’s underlying logic to provide effective automation...

• Athena

• Referenced in 10 articles [sw09967]
• programming language, Athena is a higher-order functional language in the tradition of Scheme ... many-sorted first-order logic. Many-sorted first-order logic is a very expressive language ... Manzano in her ”Extensions of first-order logic”) have argued that it can be viewed ... framework for all other logics, including higher-order logic. It retains the tractability of first...

• THF0

• Referenced in 11 articles [sw03310]
• higher-order logic. Maintaining a consistent style between the first-order and higher-order languages...

• Predator

• Referenced in 13 articles [sw07396]
• inspired by works on separation logic with higher-order list predicates, but they...

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