Abstract
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. © Springer-Verlag 2013.
Cite
CITATION STYLE
Dietrich, D., Whiteside, I., & Aspinall, D. (2013). Polar: A framework for proof refactoring. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8312 LNCS, pp. 776–791). https://doi.org/10.1007/978-3-642-45221-5_52
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
