Sciweavers

TPHOL
2002
IEEE
13 years 12 months ago
Weakest Precondition for General Recursive Programs Formalized in Coq
Abstract. This paper describes a formalization of the weakest precondition, wp, for general recursive programs using the type-theoretical proof assistant Coq. The formalization is ...
Xingyuan Zhang, Malcolm Munro, Mark Harman, Lin Hu