An interactive extension mechanism for reusing verified programs
Sosuke Moriguchi, Takuo Watanabe · 2013
Interactive theorem provers such as Coq are widely used for program verification. However, if one aims to, for example, add a simple feature to an already-verified program, it may require reconstructing the entire proof. In other words, building upon a verified program (a program with its accompanying proofs) while also maintaining its consistency is generally not an easy task.