Weakest Precondition for General Recursive Programs Formalized in Coq

Xingyuan Zhang, Malcolm Munro, Mark Harman, Lin Hu. Weakest Precondition for General Recursive Programs Formalized in Coq. In Victor Carreño, César Muñoz, Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings. Volume 2410 of Lecture Notes in Computer Science, pages 332-348, Springer, 2002. [doi]

@inproceedings{ZhangMHH02,
  title = {Weakest Precondition for General Recursive Programs Formalized in Coq},
  author = {Xingyuan Zhang and Malcolm Munro and Mark Harman and Lin Hu},
  year = {2002},
  url = {http://link.springer.de/link/service/series/0558/bibs/2410/24100332.htm},
  researchr = {https://researchr.org/publication/ZhangMHH02},
  cites = {0},
  citedby = {0},
  pages = {332-348},
  booktitle = {Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings},
  editor = {Victor Carreño and César Muñoz and Sofiène Tahar},
  volume = {2410},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-44039-9},
}