Polar swMATH ID: 7906 Software Authors: Dietrich, Dominik; Whiteside, Iain; Aspinall, David Description: Polar: a framework for proof refactoring We present a prototype refactoring framework based on graph rewriting and bidirectional transformations that is designed to be generic, extensible, and declarative. Our approach uses a language-independent graph meta-model to represent proof developments in a generic way. We use graph rewriting to enrich the meta-model with dependency information and to perform refactorings, which are written as declarative rewrite rules. Our framework, called Polar, is implemented in the GrGen rewriting engine. Homepage: http://rd.springer.com/chapter/10.1007%2F978-3-642-45221-5_52 Related Software: OpenTheory; CoqHammer; Lean; Jitawa; HOLyHammer; Flyspeck; Milawa; ileanCoP; QMT; MMT; HOL Light; Matita; HOL; Mizar; MoMM; Eiffel; MPTP 0.2; Isabelle/HOL; Isabelle; Coq Cited in: 2 Publications Cited by 5 Authors 1 Aspinall, David 1 Dietrich, Dominik 1 Gauthier, Thibault 1 Kaliszyk, Cezary 1 Whiteside, Iain Cited in 1 Serial 1 Journal of Symbolic Computation Cited in 1 Field 2 Computer science (68-XX) Citations by Year