Paper Info
Title
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 a deep embedding using the computational power intrinsic to type theory. Since Coq accepts only structural recursive functions, the computational embedding of general recursive programs is non-trivial. To justify the embedding, an operational semantics is defined and the equivalence between wp and the operational semantics is proved. Three major healthiness conditions, namely: Strictness, Monotonicity and Conjunctivity are proved as well.
Year
Venue
Keywords
2002
TPHOLs
weakest precondition,general recursive program,type theory,type-theoretical proof assistant,structural recursive function,general recursive programs,operational semantics,computational embedding,major healthiness condition,computational power,deep embedding,formal verification,proof assistant
Field
DocType
ISBN
Programming language,Computer science,Type theory,Theoretical computer science,Recursion,Distributed computing,Predicate transformer semantics,Operational semantics,Embedding,Automated theorem proving,Algorithm,Formal verification,Proof assistant
Conference
3-540-44039-9
Citations 
PageRank 
References 
7
0.59
10
Authors
4
Name
Order
Citations
PageRank
xingyuan zhang11069.80
Malcolm Munro2877199.56
Mark Harman310264389.82
Lin Hu41469.44