GhostRewriter

Interactive theorem provers (ITPs) address challenges in both programming and mathematics. Computation enhances their efficiency and usability, but users have little or no control over it. We aim to refine control over computation in ITPs by drawing on ideas from deductive verification, namely ghost data, to enable more expressive and modular proof development.