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

Citations by Year