Zhang, X., Munro, M., Harman, M., & Hu, L. (2002, January). Weakest precondition for general recursive programs formalized in coq. Presented at 15th International Conference on Theorem Proving in Higher Order Logics : TPHOLs., Hampton, VA