HOL

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 357 articles , 1 standard article )

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

1 2 3 ... 16 17 18 next

  1. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  2. Abdulaziz, Mohammad; Norrish, Michael; Gretton, Charles: Formally verified algorithms for upper-bounding state space diameters (2018)
  3. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  4. Farmer, William M.: Incorporating quotation and evaluation into Church’s type theory (2018)
  5. Melham, Tom: Symbolic trajectory evaluation (2018)
  6. Shankar, Natarajan: Combining model checking and deduction (2018)
  7. Shi, Ling; Zhao, Yongxin; Liu, Yang; Sun, Jun; Dong, Jin Song; Qin, Shengchao: A UTP semantics for communicating processes with shared variables and its formal encoding in PVS (2018)
  8. Shi, Zhiping; Wu, Aixuan; Yang, Xiumei; Guan, Yong; Li, Yongdong; Song, Xiaoyu: Formal analysis of the kinematic Jacobian in screw theory (2018)
  9. Zhao, Chunna; Li, Shanshan: Formalization of fractional order PD control systems in HOL4 (2018)
  10. Benzmüller, Christoph: Cut-elimination for quantified conditional logic (2017)
  11. Berger, Ulrich; Hou, Tie: A realizability interpretation of Church’s simple theory of types (2017)
  12. Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
  13. Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Soundness and completeness proofs by coinductive methods (2017)
  14. Bowles, Juliana; Caminati, Marco B.: A verified algorithm enumerating event structures (2017)
  15. Farmer, William M.: Theory morphisms in Church’s type theory with quotation and evaluation (2017)
  16. Gilbert, Frédéric: Proof certificates in PVS (2017)
  17. Jha, Susmit; Seshia, Sanjit A.: A theory of formal synthesis via inductive learning (2017)
  18. Kunčar, Ondřej; Popescu, Andrei: Comprehending Isabelle/HOL’s consistency (2017)
  19. Sandberg Ericsson, Adam; Myreen, Magnus O.; Åman Pohjola, Johannes: A verified generational garbage collector for CakeML (2017)
  20. Sewell, Thomas; Kam, Felix; Heiser, Gernot: High-assurance timing analysis for a high-assurance real-time operating system (2017)

1 2 3 ... 16 17 18 next