Interactive theorem provers (e g Coq, Isabelle, HOL4, PVS) have been widely used for various verification projects, where mechanised proofs have been written by humans and checked by computers When building such mechanised proofs, we often deploy a technique called "proof by reflection " or "proof by computation " In this talk, I will share my experience of certifying computational procedures in computer algebra and building proof tactics based on those verified procedures

Interactive theorem provers (e.g. Coq, Isabelle, HOL4, PVS) have been widely used for various verification projects, where mechanised proofs have been written by humans and checked by computers. When building such mechanised proofs, we often deploy a technique called "proof by reflection" or "proof by computation". In this talk, I will share my experience of certifying computational procedures in computer algebra and building proof tactics based on those verified procedures.