ProofPower

ProofPower is a specification and proof tool based on an implementation of Higher Order Logic (HOL), following the LCF paradigm, in Standard ML. ProofPower provides support for specification and proof in Z using a semantic embedding of Z into HOL. The DAZ tool supporting refinement of Z to the SPARK subset of Ada is also available.


References in zbMATH (referenced in 57 articles )

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

1 2 3 next

  1. Abrahamsson, Oskar: A verified proof checker for higher-order logic (2020)
  2. Sheng, Feng; Zhu, Huibiao; He, Jifeng; Yang, Zongyuan; Bowen, Jonathan P.: Theoretical and practical approaches to the denotational semantics for MDESL based on UTP (2020)
  3. Kunčar, Ondřej; Popescu, Andrei: A consistent foundation for Isabelle/HOL (2019)
  4. Lin, Yuhui; Bundy, Alan; Grov, Gudmund; Maclean, Ewen: Automating Event-B invariant proofs by rippling and proof patching (2019)
  5. Ribeiro, Pedro; Cavalcanti, Ana: Angelic processes for CSP via the UTP (2019)
  6. Zhan, Bohua: Formalization of the fundamental group in untyped set theory using auto2 (2019)
  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. da Costa Cavalheiro, Simone André; Foss, Luciana; Ribeiro, Leila: Theorem proving graph grammars with attributes and negative application conditions (2017)
  9. Gilbert, Frédéric: Proof certificates in PVS (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. Arthan, Rob: On definitions of constants and types in HOL (2016)
  13. Arthan, Robin Denis: Now (f) is continuous (exercise!) (2016)
  14. Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Formalization of real analysis: a survey of proof assistants and libraries (2016)
  15. Carneiro, Mario M.: Conversion of HOL Light proofs into metamath (2016)
  16. Foster, Simon; Zeyda, Frank; Woodcock, Jim: Unifying heterogeneous state-spaces with lenses (2016)
  17. Kohlhase, Michael; Rabe, Florian: QED reloaded: towards a pluralistic formal library of mathematical knowledge (2016)
  18. Lin, Yuhui; Grov, Gudmund; Arthan, Rob: Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC (2016)
  19. Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Witnessing (co)datatypes (2015)
  20. Cheng, Shu; Woodcock, Jim; D’Souza, Deepak: Using formal reasoning on a model of tasks for FreeRTOS (2015)

1 2 3 next


Further publications can be found at: http://www.lemma-one.com/ProofPower/papers/papers.html