Polar: A Framework for Proof Refactoring

Dominik Dietrich, Iain Whiteside, David Aspinall

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning
EditorsKen McMillan, Aart Middeldorp, Andrei Voronkov
PublisherSpringer Berlin Heidelberg
Pages776-791
Number of pages16
Volume8312
ISBN (Electronic)978-3-642-45221-5
ISBN (Print)978-3-642-45220-8
DOIs
Publication statusPublished - 2013
Event19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2013 - Stellenbosch, United Kingdom
Duration: 14 Dec 201319 Dec 2013

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume8312

Conference

Conference19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2013
Country/TerritoryUnited Kingdom
CityStellenbosch
Period14/12/1319/12/13

Fingerprint

Dive into the research topics of 'Polar: A Framework for Proof Refactoring'. Together they form a unique fingerprint.

Cite this