Higher Order Logic (HOL) is a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems. An Oracle mechanism gives access to external programs such as SAT and BDD engines. HOL 4 is particularly suitable as a platform for implementing combinations of deduction, execution, and property checking. (Source: http://freecode.com/)

References in zbMATH (referenced in 293 articles , 1 standard article )

Showing results 1 to 20 of 293.
Sorted by year (citations)

1 2 3 ... 13 14 15 next

  1. Benzmüller, Christoph: Cut-elimination for quantified conditional logic (2017)
  2. Berger, Ulrich; Hou, Tie: A realizability interpretation of Church’s simple theory of types (2017)
  3. Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
  4. Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Soundness and completeness proofs by coinductive methods (2017)
  5. Bowles, Juliana; Caminati, Marco B.: A verified algorithm enumerating event structures (2017)
  6. Farmer, William M.: Theory morphisms in Church’s type theory with quotation and evaluation (2017)
  7. Jha, Susmit; Seshia, Sanjit A.: A theory of formal synthesis via inductive learning (2017)
  8. Kunčar, Ondřej; Popescu, Andrei: Comprehending Isabelle/HOL’s consistency (2017)
  9. Sewell, Thomas; Kam, Felix; Heiser, Gernot: High-assurance timing analysis for a high-assurance real-time operating system (2017)
  10. Zeyda, Frank; Foster, Simon; Freitas, Leo: An axiomatic value model for Isabelle/UTP (2017)
  11. Adams, Mark: HOL zero’s solutions for Pollack-inconsistency (2016)
  12. Ahmed, Waqar; Hasan, Osman; Tahar, Sofiène: Formalization of reliability block diagrams in higher-order logic (2016)
  13. Ahmed, Waqar; Hasan, Osman; Tahar, Sofiène: Formal dependability modeling and analysis: a survey (2016)
  14. Arthan, Rob: On definitions of constants and types in HOL (2016)
  15. Bengtson, Jesper; Parrow, Joachim; Weber, Tjark: Psi-calculi in Isabelle (2016)
  16. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  17. Farmer, William M.: Incorporating quotation and evaluation into Church’s type theory: syntax and semantics (2016)
  18. Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (2016)
  19. Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definitions in higher-order logic (2016)
  20. Qasim, Muhammad; Hasan, Osman; Elleuch, Maissa; Tahar, Sofiène: Formalization of normal random variables in HOL (2016)

1 2 3 ... 13 14 15 next