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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element